clarified bires_inst_tac: retain internal exceptions;
authorwenzelm
Tue, 14 Feb 2012 22:27:33 +0100
changeset 46476 dac966e4e51d
parent 46475 22eaaf4f00a3
child 46482 f310e9eabf60
clarified bires_inst_tac: retain internal exceptions;
src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Tue Feb 14 22:22:01 2012 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Tue Feb 14 22:27:33 2012 +0100
@@ -269,9 +269,7 @@
               (Thm.lift_rule cgoal thm)
       in
         compose_tac (bires_flag, rule, nprems_of thm) i
-      end) i st
-           handle TERM (msg,_)   => (warning msg; no_tac st)
-                | THM  (msg,_,_) => (warning msg; no_tac st);
+      end) i st;
   in tac end;
 
 val res_inst_tac = bires_inst_tac false;