--- a/ProgTutorial/Parsing.thy	Mon May 17 17:27:21 2010 +0100
+++ b/ProgTutorial/Parsing.thy	Mon May 17 18:20:48 2010 +0100
@@ -41,8 +41,8 @@
   "Pure/General/scan.ML"}. The second part of the library consists of
   combinators for dealing with specific token types, which are defined in the
   structure @{ML_struct OuterParse} in the file @{ML_file
-  "Pure/Isar/outer_parse.ML"}. In addition specific parsers for packages are 
-  defined in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments 
+  "Pure/Isar/parse.ML"}. In addition specific parsers for packages are 
+  defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments 
   are defined in @{ML_file "Pure/Isar/args.ML"}.
   \end{readmore}
 
@@ -480,7 +480,7 @@
 
   \begin{readmore}
   The parser functions for the theory syntax are contained in the structure
-  @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/outer_parse.ML"}.
+  @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/parse.ML"}.
   The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
   \end{readmore}
 
@@ -910,7 +910,7 @@
 text_raw {*
   \begin{exercise}
   Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
-  in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
+  in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds
   to the ``where-part'' of the introduction rules given above. Below
   we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
   purposes.