src/HOL/Tools/inductive_realizer.ML
changeset 54742 7a86358a3c0b
parent 52788 da1fdbfebd39
child 55235 4b4627f5912b
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -393,11 +393,11 @@
     1.4          val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
     1.5          val thm = Goal.prove_global thy []
     1.6            (map attach_typeS prems) (attach_typeS concl)
     1.7 -          (fn {prems, ...} => EVERY
     1.8 +          (fn {context = ctxt, prems} => EVERY
     1.9            [rtac (#raw_induct ind_info) 1,
    1.10 -           rewrite_goals_tac rews,
    1.11 +           rewrite_goals_tac ctxt rews,
    1.12             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
    1.13 -             [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
    1.14 +             [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
    1.15                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    1.16          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
    1.17            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
    1.18 @@ -459,8 +459,8 @@
    1.19              [cut_tac (hd prems) 1,
    1.20               etac elimR 1,
    1.21               ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
    1.22 -             rewrite_goals_tac rews,
    1.23 -             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
    1.24 +             rewrite_goals_tac ctxt rews,
    1.25 +             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
    1.26                 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    1.27          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
    1.28            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy