src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 33955 fff6f11b1f09
parent 33832 cff42395c246
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -77,8 +77,8 @@
     1.4        subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
     1.5      val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
     1.6      val recTs = get_rec_types descr' sorts;
     1.7 -    val newTs = Library.take (length (hd descr), recTs);
     1.8 -    val oldTs = Library.drop (length (hd descr), recTs);
     1.9 +    val newTs = (uncurry take) (length (hd descr), recTs);
    1.10 +    val oldTs = (uncurry drop) (length (hd descr), recTs);
    1.11      val sumT = if null leafTs then HOLogic.unitT
    1.12        else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    1.13      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    1.14 @@ -193,7 +193,7 @@
    1.15                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    1.16                (resolve_tac rep_intrs 1)))
    1.17                  (types_syntax ~~ tyvars ~~
    1.18 -                  (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
    1.19 +                  ((uncurry take) (length newTs, rep_set_names)) ~~ new_type_names) ||>
    1.20        Sign.add_path big_name;
    1.21  
    1.22      (*********************** definition of constructors ***********************)
    1.23 @@ -472,7 +472,7 @@
    1.24        iso_inj_thms_unfolded;
    1.25  
    1.26      val iso_thms = if length descr = 1 then [] else
    1.27 -      Library.drop (length newTs, split_conj_thm
    1.28 +      (uncurry drop) (length newTs, split_conj_thm
    1.29          (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
    1.30             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.31              REPEAT (rtac TrueI 1),