--- 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)))

--- a/Nominal/nominal_eqvt.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_eqvt.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -126,7 +126,7 @@
 
 
 val _ =
-  Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl)
+  Outer_Syntax.local_theory @{command_spec "equivariance"}
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       (Parse.xname >> equivariance_cmd)
 

--- a/Nominal/nominal_termination.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_termination.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -106,7 +106,7 @@
      (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
+  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
     "prove termination of a recursive function"
       (option_parser -- Scan.option Parse.term >> 
         (fn ((is_nominal, is_eqvt), opt_trm) =>