tuned;

--- a/src/HOL/Tools/cnf.ML	Thu Apr 10 10:30:32 2014 +0200
+++ b/src/HOL/Tools/cnf.ML	Thu Apr 10 10:36:29 2014 +0200
@@ -207,9 +207,9 @@
       in
         make_nnf_iff OF [thm1, thm2, thm3, thm4]
       end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
+  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
       make_nnf_not_false
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
+  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
       make_nnf_not_true
   | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
       let

--- 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