diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Wed Oct 26 12:59:44 2011 +0100
@@ -764,11 +764,11 @@
   Another important antiquotation is @{text "@{context}"}. (What the
   difference between a theory and a context is will be described in Chapter
   \ref{chp:advanced}.) A context is for example needed in order to use the
-  function @{ML print_abbrevs in ProofContext} that list of all currently
+  function @{ML print_abbrevs in Proof_Context} that list of all currently
   defined abbreviations.
 
   @{ML_response_fake [display, gray]
-  "ProofContext.print_abbrevs @{context}"
+  "Proof_Context.print_abbrevs @{context}"
 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
 INTER \<equiv> INFI
 Inter \<equiv> Inf
@@ -857,7 +857,7 @@
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun term_pat (ctxt, str) =
-     str |> ProofContext.read_term_pattern ctxt
+     str |> Proof_Context.read_term_pattern ctxt
          |> ML_Syntax.print_term
          |> ML_Syntax.atomic
 in
@@ -869,7 +869,7 @@
 text {*
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
-  ProofContext} (Line 5); the next two lines transform the term into a string
+  Proof_Context} (Line 5); the next two lines transform the term into a string
   so that the ML-system can understand it. (All these functions will be explained
   in more detail in later sections.) An example for this antiquotation is: