src/HOL/Nominal/nominal_induct.ML
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4    val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     1.5      (string * typ) list -> (string * typ) list list -> thm list ->
     1.6      thm list -> int -> RuleCases.cases_tactic
     1.7 -  val nominal_induct_method: Method.src -> Proof.context -> Proof.method
     1.8 +  val nominal_induct_method: (Proof.context -> Proof.method) context_parser
     1.9  end =
    1.10  struct
    1.11  
    1.12 @@ -152,11 +152,10 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun nominal_induct_method src =
    1.17 -  Method.syntax
    1.18 -   (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.19 -    avoiding -- fixing -- rule_spec) src
    1.20 -  #> (fn ((((x, y), z), w), ctxt) =>
    1.21 +val nominal_induct_method =
    1.22 +  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.23 +  avoiding -- fixing -- rule_spec >>
    1.24 +  (fn (((x, y), z), w) => fn ctxt =>
    1.25      RAW_METHOD_CASES (fn facts =>
    1.26        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
    1.27