--- a/src/HOL/Nominal/nominal_atoms.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 17 23:54:15 2010 +0200
@@ -1004,10 +1004,10 @@
(* syntax und parsing *)
-structure P = OuterParse and K = OuterKeyword;
+structure P = Parse and K = Keyword;
val _ =
- OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
- (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
+ Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+ (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;