src/HOL/Nominal/nominal_inductive.ML
 changeset 36960 01594f816e3a parent 36692 54b64d4ad524 child 38549 d0385f2764d8
```     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 15:11:25 2010 +0200
1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 23:54:15 2010 +0200
1.3 @@ -672,23 +672,20 @@
1.4
1.5  (* outer syntax *)
1.6
1.7 -local structure P = OuterParse and K = OuterKeyword in
1.8 -
1.9 -val _ = OuterKeyword.keyword "avoids";
1.10 +val _ = Keyword.keyword "avoids";
1.11
1.12  val _ =
1.13 -  OuterSyntax.local_theory_to_proof "nominal_inductive"
1.14 -    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
1.15 -    (P.xname -- Scan.optional (P.\$\$\$ "avoids" |-- P.and_list1 (P.name --
1.16 -      (P.\$\$\$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
1.17 +  Outer_Syntax.local_theory_to_proof "nominal_inductive"
1.18 +    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
1.19 +    Keyword.thy_goal
1.20 +    (Parse.xname -- Scan.optional (Parse.\$\$\$ "avoids" |-- Parse.and_list1 (Parse.name --
1.21 +      (Parse.\$\$\$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
1.22          prove_strong_ind name avoids));
1.23
1.24  val _ =
1.25 -  OuterSyntax.local_theory "equivariance"
1.26 -    "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
1.27 -    (P.xname -- Scan.optional (P.\$\$\$ "[" |-- P.list1 P.name --| P.\$\$\$ "]") [] >>
1.28 +  Outer_Syntax.local_theory "equivariance"
1.29 +    "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
1.30 +    (Parse.xname -- Scan.optional (Parse.\$\$\$ "[" |-- Parse.list1 Parse.name --| Parse.\$\$\$ "]") [] >>
1.31        (fn (name, atoms) => prove_eqvt name atoms));
1.32
1.33 -end;
1.34 -
1.35  end
```