src/HOL/Nominal/nominal_inductive.ML
 changeset 46949 94aa7b81bcf6 parent 46947 b8c7eb0c2f89 child 46961 5c6955f487e5
```     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 19:48:19 2012 +0100
1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 20:07:00 2012 +0100
1.3 @@ -673,14 +673,14 @@
1.4    Outer_Syntax.local_theory_to_proof "nominal_inductive"
1.5      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
1.6      Keyword.thy_goal
1.7 -    (Parse.xname -- Scan.optional (Parse.\$\$\$ "avoids" |-- Parse.and_list1 (Parse.name --
1.8 -      (Parse.\$\$\$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
1.9 +    (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
1.10 +      (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
1.11          prove_strong_ind name avoids));
1.12
1.13  val _ =
1.14    Outer_Syntax.local_theory "equivariance"
1.15      "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
1.16 -    (Parse.xname -- Scan.optional (Parse.\$\$\$ "[" |-- Parse.list1 Parse.name --| Parse.\$\$\$ "]") [] >>
1.17 +    (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
1.18        (fn (name, atoms) => prove_eqvt name atoms));
1.19
1.20  end
```