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