diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -226,7 +226,7 @@
     val l = k - j;
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
-      (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
+      (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys));
   in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun contains_dictvar t =
@@ -773,7 +773,7 @@
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
-            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
+            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t)
               (constrs ~~ ts_clause);
       in ((t, ty), clauses) end;
   in
@@ -788,7 +788,7 @@
   if length ts < num_args then
     let
       val k = length ts;
-      val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
+      val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
       val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
       val vs = Name.names ctxt "a" tys;
     in
@@ -797,8 +797,8 @@
       #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
     end
   else if length ts > num_args then
-    translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
-    ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
+    translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts))
+    ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
     #>> (fn (t, ts) => t `$$ ts)
   else
     translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)