diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_atoms.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -76,14 +76,10 @@
   end;
 
 (** outer syntax **)
-
-local structure P = Parse and K = Keyword in
-
 val _ =
-  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)));
+  Outer_Syntax.command ("atom_decl", Keyword.thy_decl) 
+    "declaration of a concrete atom type" 
+      ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
+        (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
 
 end;
-
-end;