tuned;

--- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -383,7 +383,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
                  |> fold_rev implies_intr (map cprop_of newgoals @ steps)
-                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
+                 |> Drule.generalize ([], [Rn])
 
     val nbranches = length branches
     val npres = length pres

--- a/src/Pure/more_thm.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/Pure/more_thm.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -279,9 +279,10 @@
 
 val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
 
-fun forall_elim_var i th = forall_elim_vars_aux
-  (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
-  | _ => raise THM ("forall_elim_vars", i, [th])) i th;
+fun forall_elim_var i th =
+  forall_elim_vars_aux
+    (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
+      | _ => raise THM ("forall_elim_vars", i, [th])) i th;
 
 end;
 

--- a/src/Pure/term.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/Pure/term.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -467,7 +467,7 @@
 val add_tvars = fold_types add_tvarsT;
 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
-val add_tfree_namesT = fold_atyps (fn TFree (xi, _) => insert (op =) xi | _ => I);
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
 val add_tfree_names = fold_types add_tfree_namesT;
 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
 val add_tfrees = fold_types add_tfreesT;

--- a/src/Pure/thm.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/Pure/thm.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -1068,8 +1068,9 @@
         val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th;
         val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
 
-        val bad_type = if null tfrees then K false else
-          Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
+        val bad_type =
+          if null tfrees then K false
+          else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
         fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x
           | bad_term (Var (_, T)) = bad_type T
           | bad_term (Const (_, T)) = bad_type T