diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_atoms.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -77,7 +77,7 @@
 
 (** outer syntax **)
 val _ =
-  Outer_Syntax.command ("atom_decl", Keyword.thy_decl) 
+  Outer_Syntax.command @{command_spec "atom_decl"}
     "declaration of a concrete atom type" 
       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
         (Toplevel.print oo (Toplevel.theory o add_atom_decl)))