src/Tools/induct.ML
changeset 53168 d998de7f0efc
parent 52732 b4da1f2ec73f
child 54742 7a86358a3c0b
     1.1 --- a/src/Tools/induct.ML	Fri Aug 23 15:36:54 2013 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri Aug 23 17:01:12 2013 +0200
     1.3 @@ -919,7 +919,7 @@
     1.4  
     1.5  val cases_setup =
     1.6    Method.setup @{binding cases}
     1.7 -    (Args.mode no_simpN --
     1.8 +    (Scan.lift (Args.mode no_simpN) --
     1.9        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.10        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.11          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.12 @@ -928,8 +928,9 @@
    1.13  
    1.14  fun gen_induct_setup binding itac =
    1.15    Method.setup binding
    1.16 -    (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.17 -      (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.18 +    (Scan.lift (Args.mode no_simpN) --
    1.19 +      (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.20 +        (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.21        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    1.22          RAW_METHOD_CASES (fn facts =>
    1.23            Seq.DETERM