src/HOL/Tools/Function/induction_schema.ML

     val (branches, steps) =
       map_index prove_branch (branches ~~ (complete_thms ~~ pats))
       |> split_list |> apsnd flat
 
     val istep = sum_split_rule
-      |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+      |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
       |> Thm.implies_intr ihyp
       |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
 
     val induct_rule =
       @{thm "wf_induct_rule"}