--- 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)));