diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -74,8 +74,8 @@
       let
         val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
         val (Us', U') = strip_type T;
-        val Us = Library.take (length ts, Us');
-        val U = Library.drop (length ts, Us') ---> U';
+        val Us = (uncurry take) (length ts, Us');
+        val U = (uncurry drop) (length ts, Us') ---> U';
         val T' = maps HOLogic.flatten_tupleT Us ---> U;
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let