--- a/ProgTutorial/First_Steps.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -856,7 +856,7 @@
   of this antiquotation is that it does not allow you to use schematic
   variables in terms. If you want to have an antiquotation that does not have
   this restriction, you can implement your own using the function @{ML_ind
-  inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code
+  inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code
   for the antiquotation @{text "term_pat"} is as follows.
 *}
 
@@ -869,7 +869,7 @@
          |> ML_Syntax.print_term
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
+  ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat)
 end*}
 
 text {*
@@ -906,7 +906,7 @@
           |> ML_Syntax.atomic
       end
 in
-  ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
+  ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
 
 text {*
@@ -921,9 +921,9 @@
   code harder to read, than making it easier. 
 
   \begin{readmore}
-  The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
-  for most antiquotations. Most of the basic operations on ML-syntax are implemented 
-  in @{ML_file "Pure/ML/ml_syntax.ML"}.
+  The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
+  contain the infrastructure and definitions for most antiquotations. Most of the basic operations 
+  on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
   \end{readmore}
 *}