src/HOL/Tools/Function/induction_scheme.ML

       val aihyp = assume ihyp
 
      (* Rule for case splitting along the sum types *)
       val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
       val pats = map_index (uncurry inject) xss
-      val sum_split_rule = FundefDatatype.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
 
       fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
           let
             val fxs = map Free xs
             val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))