--- a/src/HOL/Tools/old_primrec.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Wed Nov 25 09:13:46 2009 +0100
@@ -124,8 +124,8 @@
let
val fnameT' as (fname', _) = dest_Const f;
val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
- val ls = (uncurry take) (rpos, ts);
- val rest = (uncurry drop) (rpos, ts);
+ val ls = take rpos ts;
+ val rest = drop rpos ts;
val (x', rs) = (hd rest, tl rest)
handle Empty => raise RecError ("not enough arguments\
\ in recursive application\nof function " ^ quote fname' ^ " on rhs");