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