src/HOL/Tools/record.ML
changeset 54742 7a86358a3c0b
parent 54707 0b3a4bdfc3d1
child 54895 515630483010
     1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -1616,9 +1616,9 @@
     1.4  
     1.5      val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
     1.6        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
     1.7 -        (fn _ =>
     1.8 +        (fn {context = ctxt, ...} =>
     1.9            EVERY1
    1.10 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
    1.11 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
    1.12              etac @{thm meta_allE}, atac,
    1.13              rtac (@{thm prop_subst} OF [surject]),
    1.14              REPEAT o etac @{thm meta_allE}, atac]));
    1.15 @@ -1742,12 +1742,13 @@
    1.16          HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.17            (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
    1.18             Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
    1.19 -      fun tac eq_def =
    1.20 +      fun tac ctxt eq_def =
    1.21          Class.intro_classes_tac []
    1.22 -        THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
    1.23 +        THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
    1.24          THEN ALLGOALS (rtac @{thm refl});
    1.25        fun mk_eq thy eq_def =
    1.26 -        rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    1.27 +        rewrite_rule (Proof_Context.init_global thy)
    1.28 +          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    1.29        fun mk_eq_refl thy =
    1.30          @{thm equal_refl}
    1.31          |> Thm.instantiate
    1.32 @@ -1765,8 +1766,7 @@
    1.33        |-> (fn eq => Specification.definition
    1.34              (NONE, (Attrib.empty_binding, eq)))
    1.35        |-> (fn (_, (_, eq_def)) =>
    1.36 -         Class.prove_instantiation_exit_result Morphism.thm
    1.37 -            (fn _ => fn eq_def => tac eq_def) eq_def)
    1.38 +         Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
    1.39        |-> (fn eq_def => fn thy =>
    1.40              thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
    1.41        |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
    1.42 @@ -2139,18 +2139,18 @@
    1.43  
    1.44      val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
    1.45        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
    1.46 -        (fn _ =>
    1.47 +        (fn {context = ctxt', ...} =>
    1.48            EVERY1
    1.49 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
    1.50 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
    1.51              etac @{thm meta_allE}, atac,
    1.52              rtac (@{thm prop_subst} OF [surjective]),
    1.53              REPEAT o etac @{thm meta_allE}, atac]));
    1.54  
    1.55      val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
    1.56        Goal.prove_sorry_global defs_thy [] [] split_object_prop
    1.57 -        (fn _ =>
    1.58 +        (fn {context = ctxt, ...} =>
    1.59            rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
    1.60 -          rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
    1.61 +          rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
    1.62            rtac split_meta 1));
    1.63  
    1.64      val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>