# HG changeset patch
# User lcp
# Date 755516199 -3600
# Node ID fe5d88d4c7e1da937e724a26efcf9dd71800d8c9
# Parent  4ae10fc91cba25267700bcae441822e47b4901e6
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.

diff -r 4ae10fc91cba -r fe5d88d4c7e1 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Dec 09 11:39:33 1993 +0100
+++ b/src/Pure/tactic.ML	Fri Dec 10 10:36:39 1993 +0100
@@ -206,7 +206,7 @@
 	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
 			nsubgoal) i
 	   handle TERM (msg,_) => (writeln msg;  no_tac)
-		| THM _ => no_tac );
+		| THM  (msg,_,_) => (writeln msg;  no_tac) );
 
 (*Resolve version*)
 fun res_inst_tac sinsts rule i =