src/HOL/Tools/Function/pat_completeness.ML

--- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Jun 27 12:34:58 2013 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Jun 27 17:06:22 2013 +0200
@@ -152,7 +152,7 @@
     val complete_thm = prove_completeness ctxt xs thesis qss patss
       |> fold_rev (Thm.forall_intr o cterm_of thy) vs
     in
-      PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
+      PRIMITIVE (fn st => Drule.compose (complete_thm, i, st))
   end
   handle COMPLETENESS => no_tac)