src/Tools/induction.ML
changeset 56506 c1f04411d43f
parent 45014 0e847655b2d8
child 58826 2ed2eaabe3df
--- 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