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 12:43:25 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13440;
          Tue, 15 Dec 92 04:27:44 -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 AA13434;
          Tue, 15 Dec 92 04:27:31 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Tue, 15 Dec 1992 12:26:32 +0000
To: Wishnu Prasetya <wishnu@nl.ruu.cs>
Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Tom.Melham@uk.ac.cam.cl
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 12:26:08 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.147:15.11.92.12.26.37"@cl.cam.ac.uk>


>    let NO_EFFECT_TAC p = EVERY_ASSUM
>        (\thm. (let hyp = snd(dest_thm thm) in
>               let q = fst(dest_comb hyp) in
>               let r="^p=^q" in
>              ALL_TAC) ? ALL_TAC) ;;
> 
>    #set_goal(["(f:bool->bool) x"], "y:bool") ;;
>    "y"
>        [ "f x " ] 
> 
>    () : void
> 
>    #e (NO_EFFECT_TAC "x:bool") ;;
>    OK..
>    Badly typed application of:  "$= x"
>       which has type:           ":bool -> bool"
>    to the argument term:        "f"
>       which has type:           ":bool -> bool"
> 
>    "y"
>        [ "x ==> y" ]
>        [ "f x" ]
> 
>    () : void
> 
> 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.

What's happening is that the quotation "^p=^q" is generating a
failure which *is* in fact trapped by the failure trapping 
construct `?'.  Hence (the second) ALL_TAC is eventually applied.

You still see an error message because an ill-typed mk_comb 
*within a quotation* causes an error message to be *printed
to the screen*.  I.e. the message "Badly typed..." is not,
in fact, a failure string but something just printed by the
quotation parser. Richard's solution is correct --- use
explicit constructors rather than quotations.

There are, by the way, reasons why one should avoid using
in-line quotations (using antiquotations as well) within code.
Not least, it is (in theory) inefficient, as it involves the
parser.

Tom