diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Integ/cooper_dec.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -442,7 +442,7 @@
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
-    |_  => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
    end;
 
 
@@ -736,7 +736,7 @@
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
     in h p_elements
     end;