--- a/Nominal/NewParser.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/NewParser.thy	Wed May 26 15:37:56 2010 +0200
@@ -12,7 +12,7 @@
 ML {* 
 (* nominal datatype parser *)
 local
-  structure P = OuterParse;
+  structure P = Parse;
   structure S = Scan
 
   fun triple1 ((x, y), z) = (x, y, z)
@@ -21,9 +21,9 @@
   fun tswap (((x, y), z), u) = (x, y, u, z)
 in
 
-val _ = OuterKeyword.keyword "bind"
-val _ = OuterKeyword.keyword "bind_set"
-val _ = OuterKeyword.keyword "bind_res"
+val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "bind_set"
+val _ = Keyword.keyword "bind_res"
 
 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
 
@@ -42,7 +42,7 @@
 
 (* binding function parser *)
 val bnfun_parser = 
-  S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
+  S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
 
 (* main parser *)
 val main_parser =
@@ -715,7 +715,7 @@
 
 (* Command Keyword *)
 
-val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
+val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
   (main_parser >> nominal_datatype2_cmd)
 *}