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;