Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 15 Dec 1992 10:19:40 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13292;
          Tue, 15 Dec 92 02:05:14 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13287;
          Tue, 15 Dec 92 02:05:03 -0800
Received: from teal.cl.cam.ac.uk (user rjb) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Tue, 15 Dec 1992 10:04:09 +0000
To: Wishnu Prasetya <wishnu@nl.ruu.cs>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: HELP: deleting assumption.
In-Reply-To: Your message of Tue, 15 Dec 92 10:03:46 +0700. <199212150903.AA20712@infix.cs.ruu.nl>
Date: Tue, 15 Dec 92 10:03:58 +0000
From: Richard Boulton <Richard.Boulton@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.939:15.11.92.10.04.13"@cl.cam.ac.uk>

> NO_EFFECT_TAC "x:bool" results the intended effect on the goal, namely
> nothing. But I don't understand why it complains about bad type
> application. I have put the '?' trapping in case of failure. Yet the
> error message is generated, and yet the error is not relevant since it
> has no effect to the result.

The reason the failure is not trapped is that it is generated by the quotation.
I'm not sure about this, but I guess the error is occurring at the
parsing/type-checking stage rather than the evaluation stage, and that's why
it isn't trapped. Anyway, the solution is simple: use explicit constructors
instead of the quotation:

   let NO_EFFECT_TAC p = EVERY_ASSUM
       (\thm. (let hyp = snd(dest_thm thm) in
              let q = fst(dest_comb hyp) in
              let r = mk_eq(p,q) in
              ALL_TAC) ? ALL_TAC) ;;

Richard.