src/HOL/Tools/split_rule.ML
changeset 33955 fff6f11b1f09
parent 33368 b1cf34f1855c
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/split_rule.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -74,8 +74,8 @@
     1.4        let
     1.5          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
     1.6          val (Us', U') = strip_type T;
     1.7 -        val Us = Library.take (length ts, Us');
     1.8 -        val U = Library.drop (length ts, Us') ---> U';
     1.9 +        val Us = (uncurry take) (length ts, Us');
    1.10 +        val U = (uncurry drop) (length ts, Us') ---> U';
    1.11          val T' = maps HOLogic.flatten_tupleT Us ---> U;
    1.12          fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    1.13                let