1.1 --- a/src/Tools/induct.ML	Mon Aug 18 15:46:27 2014 +0200
     1.2 +++ b/src/Tools/induct.ML	Tue Aug 19 12:05:11 2014 +0200
     1.3 @@ -932,15 +932,13 @@
     1.4            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
     1.5      "case analysis on types or predicates/sets";
     1.6  
     1.7 -fun gen_induct_setup binding itac =
     1.8 +fun gen_induct_setup binding tac =
     1.9    Method.setup binding
    1.10      (Scan.lift (Args.mode no_simpN) --
    1.11        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.12          (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.13 -      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    1.14 -        RAW_METHOD_CASES (fn facts =>
    1.15 -          Seq.DETERM
    1.16 -            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    1.17 +      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
    1.18 +        Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
    1.19      "induction on types or predicates/sets";
    1.20  
    1.21  val induct_setup = gen_induct_setup @{binding induct} induct_tac;
    1.22 @@ -948,9 +946,8 @@
    1.23  val coinduct_setup =
    1.24    Method.setup @{binding coinduct}
    1.25      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    1.26 -      (fn ((insts, taking), opt_rule) => fn ctxt =>
    1.27 -        RAW_METHOD_CASES (fn facts =>
    1.28 -          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
    1.29 +      (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
    1.30 +        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
    1.31      "coinduction on types or predicates/sets";
    1.32  
    1.33  end;