explicit Simplifier.global_context;
authorwenzelm
Mon Mar 22 20:59:22 2010 +0100 (2010-03-22)
changeset 35899e810f73c8ee2
parent 35898 c890a3835d15
child 35909 a4ed7aaa7d03
explicit Simplifier.global_context;
src/HOL/Tools/Datatype/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 20:58:52 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 20:59:22 2010 +0100
     1.3 @@ -358,7 +358,7 @@
     1.4        [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
     1.5      val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
     1.6      val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     1.7 -    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
     1.8 +    val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
     1.9        (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
    1.10      fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
    1.11        |> Simpdata.mk_eq;