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