diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -671,14 +671,14 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
     (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
       (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
         prove_strong_ind name avoids));
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "equivariance"}
+  Outer_Syntax.local_theory @{command_keyword equivariance}
     "prove equivariance for inductive predicate involving nominal datatypes"
     (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
       (fn (name, atoms) => prove_eqvt name atoms));