--- a/ProgTutorial/Recipes/Antiquotes.thy	Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Thu May 27 10:39:07 2010 +0200
@@ -78,11 +78,11 @@
    ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
 val _ = ThyOutput.antiquotation "ML_checked"
-         (Scan.lift (OuterParse.position Args.name)) output_ml *}
+         (Scan.lift (Parse.position Args.name)) output_ml *}
 
 text {*
   where in Lines 1 and 2 the positional information is properly treated. The
-  parser @{ML OuterParse.position} encodes the positional information in the 
+  parser @{ML Parse.position} encodes the positional information in the 
   result.
 
   We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to
@@ -137,7 +137,7 @@
    end)
 
 val _ = ThyOutput.antiquotation "ML_resp" 
-          (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
+          (Scan.lift (Parse.position (Args.name -- Args.name))) 
              output_ml_resp*}
 
 text {*