src/HOL/Tools/Datatype/datatype_prop.ML
changeset 33955 fff6f11b1f09
parent 33338 de76079f973a
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4          end;
     1.5    in
     1.6      map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
     1.7 -      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
     1.8 +      (hd descr) ((uncurry take) (length (hd descr), get_rec_types descr' sorts))
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -82,7 +82,7 @@
    1.13    let
    1.14      val descr' = flat descr;
    1.15      val recTs = get_rec_types descr' sorts;
    1.16 -    val newTs = Library.take (length (hd descr), recTs);
    1.17 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.18  
    1.19      fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
    1.20  
    1.21 @@ -174,7 +174,7 @@
    1.22        end
    1.23  
    1.24    in map make_casedist
    1.25 -    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
    1.26 +    ((hd descr) ~~ (uncurry take) (length (hd descr), get_rec_types descr' sorts))
    1.27    end;
    1.28  
    1.29  (*************** characteristic equations for primrec combinator **************)
    1.30 @@ -257,7 +257,7 @@
    1.31      val descr' = flat descr;
    1.32      val recTs = get_rec_types descr' sorts;
    1.33      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    1.34 -    val newTs = Library.take (length (hd descr), recTs);
    1.35 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.36      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    1.37  
    1.38      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
    1.39 @@ -280,7 +280,7 @@
    1.40    let
    1.41      val descr' = flat descr;
    1.42      val recTs = get_rec_types descr' sorts;
    1.43 -    val newTs = Library.take (length (hd descr), recTs);
    1.44 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.45  
    1.46      fun make_case T comb_t ((cname, cargs), f) =
    1.47        let
    1.48 @@ -304,7 +304,7 @@
    1.49      val descr' = flat descr;
    1.50      val recTs = get_rec_types descr' sorts;
    1.51      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    1.52 -    val newTs = Library.take (length (hd descr), recTs);
    1.53 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.54      val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
    1.55      val P = Free ("P", T' --> HOLogic.boolT);
    1.56  
    1.57 @@ -415,7 +415,7 @@
    1.58    let
    1.59      val descr' = flat descr;
    1.60      val recTs = get_rec_types descr' sorts;
    1.61 -    val newTs = Library.take (length (hd descr), recTs);
    1.62 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.63  
    1.64      fun mk_eqn T (cname, cargs) =
    1.65        let