src/HOL/Tools/Datatype/datatype_codegen.ML
changeset 33955 fff6f11b1f09
parent 33553 35f2b30593a8
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -217,18 +217,18 @@
     1.4         invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
     1.5      else
     1.6        let
     1.7 -        val ts1 = Library.take (i, ts);
     1.8 -        val t :: ts2 = Library.drop (i, ts);
     1.9 +        val ts1 = (uncurry take) (i, ts);
    1.10 +        val t :: ts2 = (uncurry drop) (i, ts);
    1.11          val names = List.foldr OldTerm.add_term_names
    1.12            (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
    1.13 -        val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
    1.14 +        val (Ts, dT) = split_last ((uncurry take) (i+1, fst (strip_type T)));
    1.15  
    1.16          fun pcase [] [] [] gr = ([], gr)
    1.17            | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
    1.18                let
    1.19                  val j = length cargs;
    1.20                  val xs = Name.variant_list names (replicate j "x");
    1.21 -                val Us' = Library.take (j, fst (strip_type U));
    1.22 +                val Us' = (uncurry take) (j, fst (strip_type U));
    1.23                  val frees = map Free (xs ~~ Us');
    1.24                  val (cp, gr0) = invoke_codegen thy defs dep module false
    1.25                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;