src/Tools/Code/code_thingol.ML

   let
     val j = length ts;
     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 =
   let
     fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss

         val t = nth ts t_pos;
         val ts_clause = nth_drop t_pos ts;
         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
     translate_const thy algbr eqngr thm c_ty
     ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs

   end
 and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   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
       fold_map (translate_typ thy algbr eqngr) tys
       ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
       #>> (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)
 and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
   case Code.get_case_scheme thy c