1.1 --- a/src/Tools/induction.ML	Thu Apr 10 10:30:32 2014 +0200
     1.2 +++ b/src/Tools/induction.ML	Thu Apr 10 10:36:29 2014 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    | (p as Free _, _) => [p]
     1.5    | (_, ts) => flat(map preds_of ts))
     1.6  
     1.7 -fun name_hyps thy (arg as ((cases,consumes),th)) =
     1.8 +fun name_hyps (arg as ((cases, consumes), th)) =
     1.9    if not(forall (null o #2 o #1) cases) then arg
    1.10    else
    1.11      let
    1.12 @@ -35,7 +35,7 @@
    1.13          (take n cases ~~ take n hnamess)
    1.14      in ((cases',consumes),th) end
    1.15  
    1.16 -val induction_tac = Induct.gen_induct_tac name_hyps
    1.17 +val induction_tac = Induct.gen_induct_tac (K name_hyps)
    1.18  
    1.19  val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    1.20