src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -402,7 +402,7 @@
 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
-    val ctxt = ProofContext.init_global thy;
+    val ctxt = Proof_Context.init_global thy;
     fun read_is strs =
       map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs
       |> Syntax.check_terms ctxt;