--- a/src/HOL/Nominal/nominal_inductive.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 15 20:07:00 2012 +0100
@@ -673,14 +673,14 @@
Outer_Syntax.local_theory_to_proof "nominal_inductive"
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
Keyword.thy_goal
- (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
- (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
+ (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 "equivariance"
"prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
- (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
+ (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
end