# HG changeset patch
# User wenzelm
# Date 1329254853 -3600
# Node ID dac966e4e51d87967cc5fee13b8bb48a5f71d7c4
# Parent  22eaaf4f00a39f1ec4f302989a750d69c068cb36
clarified bires_inst_tac: retain internal exceptions;

diff -r 22eaaf4f00a3 -r dac966e4e51d 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;