--- a/src/HOL/hologic.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/hologic.ML Thu Mar 03 12:43:01 2005 +0100
@@ -148,7 +148,7 @@
fun all_const T = Const ("All", [T --> boolT] ---> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-val list_all = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P));
+val list_all = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P));
fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
@@ -237,7 +237,7 @@
(*Makes a nested tuple from a list, following the product type structure*)
fun mk_tuple (Type ("*", [T1, T2])) tms =
mk_prod (mk_tuple T1 tms,
- mk_tuple T2 (drop (length (prodT_factors T1), tms)))
+ mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
| mk_tuple T (t::_) = t;
@@ -246,13 +246,13 @@
local (*currently unused*)
-fun mk_tupleT Ts = foldr mk_prodT (Ts, unitT);
+fun mk_tupleT Ts = Library.foldr mk_prodT (Ts, unitT);
fun dest_tupleT (Type ("Product_Type.unit", [])) = []
| dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
| dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
-fun mk_tuple ts = foldr mk_prod (ts, unit);
+fun mk_tuple ts = Library.foldr mk_prod (ts, unit);
fun dest_tuple (Const ("Product_Type.Unity", _)) = []
| dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u