Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit Simplifier.global_context;
authorwenzelm
Mon, 22 Mar 2010 20:59:22 +0100
changeset 35899 e810f73c8ee2
parent 35898 c890a3835d15
child 35909 a4ed7aaa7d03
explicit Simplifier.global_context;
src/HOL/Tools/Datatype/datatype_codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 20:58:52 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 20:59:22 2010 +0100
@@ -358,7 +358,7 @@
       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
     val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
-    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
+    val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
isabelle