diff -r da8817d01e7c -r 23f352990944 doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Sat Apr 16 15:47:52 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Sat Apr 16 16:15:37 2011 +0200
@@ -314,7 +314,7 @@
   exports result @{text "thm"} from the the @{text "inner"} context
   back into the @{text "outer"} one; @{text "is_goal = true"} means
   this is a goal context.  The result is in HHF normal form.  Note
-  that @{ML "ProofContext.export"} combines @{ML "Variable.export"}
+  that @{ML "Proof_Context.export"} combines @{ML "Variable.export"}
   and @{ML "Assumption.export"} in the canonical way.
 
   \end{description}
@@ -341,7 +341,7 @@
 text {* Note that the variables of the resulting rule are not
   generalized.  This would have required to fix them properly in the
   context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML
-  Variable.export} or the combined @{ML "ProofContext.export"}).  *}
+  Variable.export} or the combined @{ML "Proof_Context.export"}).  *}
 
 
 section {* Structured goals and results \label{sec:struct-goals} *}
@@ -481,10 +481,10 @@
       |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];
   *}
   ML_prf %"ML" {*
-    singleton (ProofContext.export ctxt1 ctxt0) @{thm refl};
+    singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};
   *}
   ML_prf %"ML" {*
-    ProofContext.export ctxt1 ctxt0 [Thm.reflexive x]
+    Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
       handle ERROR msg => (warning msg; []);
   *}
 end