src/HOL/Tools/split_rule.ML

--- a/src/HOL/Tools/split_rule.ML	Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Nov 25 09:13:46 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 = (uncurry take) (length ts, Us');
-        val U = (uncurry drop) (length ts, Us') ---> U';
+        val Us = take (length ts) Us';
+        val U = drop (length ts) Us' ---> U';
         val T' = maps HOLogic.flatten_tupleT Us ---> U;
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let