src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Mon May 03 14:25:56 2010 +0200
@@ -401,7 +401,7 @@
 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun read_is strs =
       map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
       |> Syntax.check_terms ctxt;