# HG changeset patch
# User huffman
# Date 1269298971 25200
# Node ID 6943a36453e8337dbd961d7b22b9edebf03b26dd
# Parent  b0e300bd3a2c118d3487a316d93e0ab7adfdb525# Parent  2062295537e0149ca082790dec03c772bf9a01ac
merged

diff -r b0e300bd3a2c -r 6943a36453e8 src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Mon Mar 22 15:53:25 2010 -0700
+++ b/src/HOL/Predicate_Compile.thy	Mon Mar 22 16:02:51 2010 -0700
@@ -1,4 +1,3 @@
-
 (*  Title:      HOL/Predicate_Compile.thy
     Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
 *)
diff -r b0e300bd3a2c -r 6943a36453e8 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 15:53:25 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Mar 22 16:02:51 2010 -0700
@@ -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;