--- a/Nominal-General/nominal_atoms.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_atoms.ML	Fri May 21 10:42:53 2010 +0200
@@ -71,10 +71,10 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
+  Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
     ((P.binding -- Scan.option (Args.parens (P.binding))) >>
       (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
 

--- a/Nominal-General/nominal_eqvt.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_eqvt.ML	Fri May 21 10:42:53 2010 +0200
@@ -184,10 +184,10 @@
   equivariance preds raw_induct intrs ctxt |> snd
 end
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.local_theory "equivariance"
+  Outer_Syntax.local_theory "equivariance"
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       K.thy_decl (P.xname >> equivariance_cmd);
 end;

--- a/Nominal-General/nominal_permeq.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_permeq.ML	Fri May 21 10:42:53 2010 +0200
@@ -155,7 +155,7 @@
 
 
 (** methods **)
-val _ = OuterKeyword.keyword "exclude"
+val _ = Keyword.keyword "exclude"
 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   (Scan.repeat (Args.const true))) []

--- 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)
 *}