src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/axclass.ML	Mon May 03 14:25:56 2010 +0200
@@ -198,7 +198,7 @@
   (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
     SOME thm => Thm.transfer thy thm
   | NONE => error ("Unproven class relation " ^
-      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
+      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
 
 fun put_trancl_classrel ((c1, c2), th) thy =
   let
@@ -245,7 +245,7 @@
   (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
     SOME (thm, _) => Thm.transfer thy thm
   | NONE => error ("Unproven type arity " ^
-      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
+      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
 
 fun thynames_of_arity thy (c, a) =
   Symtab.lookup_list (proven_arities_of thy) a
@@ -357,7 +357,7 @@
   in (c1, c2) end;
 
 fun read_classrel thy raw_rel =
-  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
+  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
     handle TYPE (msg, _, _) => error msg;
 
 
@@ -461,7 +461,7 @@
 
 fun prove_classrel raw_rel tac thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val (c1, c2) = cert_classrel thy raw_rel;
     val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
@@ -475,7 +475,7 @@
 
 fun prove_arity raw_arity tac thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val arity = ProofContext.cert_arity ctxt raw_arity;
     val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
@@ -509,7 +509,7 @@
 
 fun define_class (bclass, raw_super) raw_params raw_specs thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val pp = Syntax.pp ctxt;
 
 
@@ -623,7 +623,7 @@
     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
 
 fun ax_arity prep =
-  axiomatize (prep o ProofContext.init) Logic.mk_arities
+  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
     (map (prefix arity_prefix) o Logic.name_arities) add_arity;
 
 fun class_const c =
@@ -643,7 +643,7 @@
 in
 
 val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
+val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
 val axiomatize_classrel = ax_classrel cert_classrel;
 val axiomatize_classrel_cmd = ax_classrel read_classrel;
 val axiomatize_arity = ax_arity ProofContext.cert_arity;