src/HOL/Nominal/nominal_atoms.ML

--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -1016,7 +1016,7 @@
 (* syntax und parsing *)
 
 val _ =
-  Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
     (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
 
 end;