src/Pure/context.ML

--- a/src/Pure/context.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/context.ML	Mon May 03 14:25:56 2010 +0200
@@ -20,7 +20,7 @@
   structure ProofContext:
   sig
     val theory_of: Proof.context -> theory
-    val init: theory -> Proof.context
+    val init_global: theory -> Proof.context
   end
 end;
 
@@ -481,7 +481,7 @@
 structure ProofContext =
 struct
   val theory_of = theory_of_proof;
-  fun init thy = Proof.Context (init_data thy, check_thy thy);
+  fun init_global thy = Proof.Context (init_data thy, check_thy thy);
 end;
 
 structure Proof_Data =
@@ -529,7 +529,7 @@
 fun proof_map f = the_proof o f o Proof;
 
 val theory_of = cases I ProofContext.theory_of;
-val proof_of = cases ProofContext.init I;
+val proof_of = cases ProofContext.init_global I;