author | wenzelm |
Tue, 14 Feb 2012 22:27:33 +0100 | |
changeset 46476 | dac966e4e51d |
parent 46475 | 22eaaf4f00a3 |
child 46482 | f310e9eabf60 |
--- 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;