src/Tools/Code/code_thingol.ML
changeset 33955 fff6f11b1f09
parent 33420 17b7095ad463
child 33957 e9afca2118d4
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4      val l = k - j;
     1.5      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     1.6      val vs_tys = (map o apfst) SOME
     1.7 -      (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
     1.8 +      (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys));
     1.9    in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
    1.10  
    1.11  fun contains_dictvar t =
    1.12 @@ -773,7 +773,7 @@
    1.13          val clauses = if null case_pats
    1.14            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
    1.15            else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
    1.16 -            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
    1.17 +            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t)
    1.18                (constrs ~~ ts_clause);
    1.19        in ((t, ty), clauses) end;
    1.20    in
    1.21 @@ -788,7 +788,7 @@
    1.22    if length ts < num_args then
    1.23      let
    1.24        val k = length ts;
    1.25 -      val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
    1.26 +      val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
    1.27        val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
    1.28        val vs = Name.names ctxt "a" tys;
    1.29      in
    1.30 @@ -797,8 +797,8 @@
    1.31        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
    1.32      end
    1.33    else if length ts > num_args then
    1.34 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
    1.35 -    ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
    1.36 +    translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts))
    1.37 +    ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
    1.38      #>> (fn (t, ts) => t `$$ ts)
    1.39    else
    1.40      translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)