diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -75,7 +75,7 @@
     let
       fun mk_branch concl =
           let
-            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+            val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
             val (P, xs) = strip_comb Pxs
           in
             SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
@@ -103,7 +103,7 @@
 
             fun mk_rcinfo pr =
                 let
-                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+                  val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
                   val (P', rcs) = strip_comb Phyp
                 in
                   (bidx P', Gvs, Gas, rcs)
@@ -151,7 +151,7 @@
        |> mk_forall_rename ("P", Pbool)
     end
 
-fun mk_wf ctxt R (IndScheme {T, ...}) =
+fun mk_wf R (IndScheme {T, ...}) =
     HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
@@ -198,8 +198,6 @@
     end
 
 
-fun mk_hol_imp a b = HOLogic.imp $ a $ b
-
 fun mk_ind_goal thy branches =
     let
       fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
@@ -256,7 +254,7 @@
             val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
                                             |> split_list
                            
-            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
+            fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
                 let
                   val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
                            
@@ -364,7 +362,7 @@
     val ineqss = mk_ineqs R scheme
                    |> map (map (pairself (assume o cert)))
     val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
-    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
+    val wf_thm = mk_wf R scheme |> cert |> assume
 
     val (descent, pres) = split_list (flat ineqss)
     val newgoals = complete @ pres @ wf_thm :: descent