src/HOL/Tools/record.ML
changeset 33955 fff6f11b1f09
parent 33711 2fdb11580b96
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/record.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4  fun rec_id i T =
     1.5    let
     1.6      val rTs = dest_recTs T;
     1.7 -    val rTs' = if i < 0 then rTs else Library.take (i, rTs);
     1.8 +    val rTs' = if i < 0 then rTs else (uncurry take) (i, rTs);
     1.9    in implode (map #1 rTs') end;
    1.10  
    1.11  
    1.12 @@ -1582,7 +1582,7 @@
    1.13        (Logic.strip_assums_concl (prop_of rule')));
    1.14      (*ca indicates if rule is a case analysis or induction rule*)
    1.15      val (x, ca) =
    1.16 -      (case rev (Library.drop (length params, ys)) of
    1.17 +      (case rev ((uncurry drop) (length params, ys)) of
    1.18          [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
    1.19            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
    1.20        | [x] => (head_of x, false));
    1.21 @@ -1635,7 +1635,7 @@
    1.22          else if len > 16 then
    1.23            let
    1.24              fun group16 [] = []
    1.25 -              | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
    1.26 +              | group16 xs = (uncurry take) (16, xs) :: group16 ((uncurry drop) (16, xs));
    1.27              val vars' = group16 vars;
    1.28              val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
    1.29            in
    1.30 @@ -1772,7 +1772,7 @@
    1.31  
    1.32  fun chunks [] [] = []
    1.33    | chunks [] xs = [xs]
    1.34 -  | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
    1.35 +  | chunks (l :: ls) xs = (uncurry take) (l, xs) :: chunks ls ((uncurry drop) (l, xs));
    1.36  
    1.37  fun chop_last [] = error "chop_last: list should not be empty"
    1.38    | chop_last [x] = ([], x)
    1.39 @@ -1881,12 +1881,12 @@
    1.40      val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
    1.41      val extension_id = implode extension_names;
    1.42  
    1.43 -    fun rec_schemeT n = mk_recordT (map #extension (Library.drop (n, parents))) extT;
    1.44 +    fun rec_schemeT n = mk_recordT (map #extension ((uncurry drop) (n, parents))) extT;
    1.45      val rec_schemeT0 = rec_schemeT 0;
    1.46  
    1.47      fun recT n =
    1.48        let val (c, Ts) = extension in
    1.49 -        mk_recordT (map #extension (Library.drop (n, parents)))
    1.50 +        mk_recordT (map #extension ((uncurry drop) (n, parents)))
    1.51            (Type (c, subst_last HOLogic.unitT Ts))
    1.52        end;
    1.53      val recT0 = recT 0;
    1.54 @@ -1896,7 +1896,7 @@
    1.55          val (args', more) = chop_last args;
    1.56          fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
    1.57          fun build Ts =
    1.58 -          fold_rev mk_ext' (Library.drop (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
    1.59 +          fold_rev mk_ext' ((uncurry drop) (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
    1.60              more;
    1.61        in
    1.62          if more = HOLogic.unit
    1.63 @@ -1989,7 +1989,7 @@
    1.64      val (accessor_thms, updator_thms, upd_acc_cong_assists) =
    1.65        timeit_msg "record getting tree access/updates:" get_access_update_thms;
    1.66  
    1.67 -    fun lastN xs = Library.drop (parent_fields_len, xs);
    1.68 +    fun lastN xs = (uncurry drop) (parent_fields_len, xs);
    1.69  
    1.70      (*selectors*)
    1.71      fun mk_sel_spec ((c, T), thm) =