diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon May 17 23:54:15 2010 +0200
@@ -204,26 +204,24 @@
 
 local
 
-structure P = OuterParse
-and K = OuterKeyword
-
 val datatypesK = "datatypes";
 val functionsK = "functions";
 val fileK = "file";
 val andK = "and"
 
-val _ = List.app K.keyword [datatypesK, functionsK];
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
 
-val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+val parse_datatype =
+  Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
 
 in
 
 val _ =
-  OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
-    K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
-      ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
-    -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
-    -- Scan.option (P.$$$ fileK |-- P.name)
+  Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+    Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+      ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+    -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+    -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
     (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));