--- a/src/HOL/Nominal/nominal_inductive.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Apr 13 18:01:05 2016 +0200
@@ -680,14 +680,14 @@
val _ =
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 --
+ (Parse.name -- 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_keyword equivariance}
"prove equivariance for inductive predicate involving nominal datatypes"
- (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
+ (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
end