--- a/Nominal/NewParser.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewParser.thy	Fri May 21 10:42:53 2010 +0200
@@ -11,7 +11,7 @@
 ML {* 
 (* nominal datatype parser *)
 local
-  structure P = OuterParse;
+  structure P = Parse;
   structure S = Scan
 
   fun triple1 ((x, y), z) = (x, y, z)
@@ -20,9 +20,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
 
@@ -41,7 +41,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 =
@@ -714,7 +714,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)
 *}