src/HOL/Tools/Function/induction_schema.ML

 (*                 |> (fn thm => (tracing (makestring thm); thm))*)
         end                  
 
     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
   in
     Thm.compose_no_flatten false (res, length newgoals) i