src/HOL/Tools/datatype_realizer.ML
changeset 59498 50b60f501b05
parent 59058 a78612c67ec0
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4              rtac (cterm_instantiate inst induct) 1,
     1.5              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
     1.6              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
     1.7 -            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
     1.8 +            REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
     1.9                REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
    1.10        |> Drule.export_without_context;
    1.11  
    1.12 @@ -194,7 +194,7 @@
    1.13              rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
    1.14              ALLGOALS (EVERY'
    1.15                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
    1.16 -               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
    1.17 +               resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
    1.18        |> Drule.export_without_context;
    1.19  
    1.20      val exh_name = Thm.derivation_name exhaust;