src/HOL/Nominal/nominal_atoms.ML

--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -947,10 +947,8 @@
 (* syntax und parsing *)
 structure P = OuterParse and K = OuterKeyword;
 
-val atom_declP =
+val _ =
   OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
     (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
 
-val _ = OuterSyntax.add_parsers [atom_declP];
-
 end;