src/HOL/Integ/cooper_dec.ML

 	        else []
     |_ => if (is_numeral t) then [dest_numeral t]  else []
    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;
 
 
 val operations = 
   [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 

       Const("True",_) => (SOME n,HOLogic.true_const)
       |F' => let val (rw,rf) = h nl 
              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;
 
 fun withness d b st vars x p = case (inf_w b d vars x p) of 
    (SOME n,_) => (SOME n,HOLogic.true_const)