--- a/src/HOL/Tools/inductive_realizer.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Jul 18 20:47:08 2015 +0200
@@ -393,11 +393,12 @@
val thm = Goal.prove_global thy []
(map attach_typeS prems) (attach_typeS concl)
(fn {context = ctxt, prems} => EVERY
- [rtac (#raw_induct ind_info) 1,
+ [resolve_tac ctxt [#raw_induct ind_info] 1,
rewrite_goals_tac ctxt rews,
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
- DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
+ DEPTH_SOLVE_1 o
+ FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]]]) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
@@ -456,11 +457,12 @@
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz')
(fn {context = ctxt, prems, ...} => EVERY
[cut_tac (hd prems) 1,
- etac elimR 1,
+ eresolve_tac ctxt [elimR] 1,
ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
rewrite_goals_tac ctxt rews,
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
- DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
+ DEPTH_SOLVE_1 o
+ FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
in