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