--- a/src/Tools/induction.ML Thu Apr 10 10:30:32 2014 +0200
+++ b/src/Tools/induction.ML Thu Apr 10 10:36:29 2014 +0200
@@ -17,7 +17,7 @@
| (p as Free _, _) => [p]
| (_, ts) => flat(map preds_of ts))
-fun name_hyps thy (arg as ((cases,consumes),th)) =
+fun name_hyps (arg as ((cases, consumes), th)) =
if not(forall (null o #2 o #1) cases) then arg
else
let
@@ -35,7 +35,7 @@
(take n cases ~~ take n hnamess)
in ((cases',consumes),th) end
-val induction_tac = Induct.gen_induct_tac name_hyps
+val induction_tac = Induct.gen_induct_tac (K name_hyps)
val setup = Induct.gen_induct_setup @{binding induction} induction_tac