Pure/tactic/compose_inst_tac: when catching exception THM, prints the
authorlcp
Fri Dec 10 10:36:39 1993 +0100 (1993-12-10)
changeset 191fe5d88d4c7e1
parent 190 4ae10fc91cba
child 192 3dc5c8016a0e
Pure/tactic/compose_inst_tac: when catching exception THM, prints the
message before failing!! This reports the reason for failure in cases like
by (res_inst_tac [("P", "?Q(a)")] mp 1);
in which ?Q appears in mp with a different type.
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Dec 09 11:39:33 1993 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Dec 10 10:36:39 1993 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4  	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
     1.5  			nsubgoal) i
     1.6  	   handle TERM (msg,_) => (writeln msg;  no_tac)
     1.7 -		| THM _ => no_tac );
     1.8 +		| THM  (msg,_,_) => (writeln msg;  no_tac) );
     1.9  
    1.10  (*Resolve version*)
    1.11  fun res_inst_tac sinsts rule i =