src/HOL/Tools/old_primrec.ML
changeset 33955 fff6f11b1f09
parent 33832 cff42395c246
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -124,8 +124,8 @@
     1.4                let
     1.5                  val fnameT' as (fname', _) = dest_Const f;
     1.6                  val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
     1.7 -                val ls = Library.take (rpos, ts);
     1.8 -                val rest = Library.drop (rpos, ts);
     1.9 +                val ls = (uncurry take) (rpos, ts);
    1.10 +                val rest = (uncurry drop) (rpos, ts);
    1.11                  val (x', rs) = (hd rest, tl rest)
    1.12                    handle Empty => raise RecError ("not enough arguments\
    1.13                     \ in recursive application\nof function " ^ quote fname' ^ " on rhs");