src/HOL/hologic.ML

--- 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