diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 14:22:36 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 14:33:07 2009 +0200
@@ -244,7 +244,7 @@
      (* 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