--- a/src/HOL/Integ/cooper_dec.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Thu Mar 03 12:43:01 2005 +0100
@@ -442,7 +442,7 @@
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
- |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+ |_ => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
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 = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+ val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
in h p_elements
end;
@@ -873,7 +873,7 @@
fun lift_qelim afn nfn qfn isat =
let fun qelim x vars p =
let val cjs = conjuncts p
- val (ycjs,ncjs) = partition (has_bound) cjs in
+ val (ycjs,ncjs) = List.partition (has_bound) cjs in
(if ycjs = [] then p else
let val q = (qfn vars ((HOLogic.exists_const HOLogic.intT
) $ Abs(x,HOLogic.intT,(list_conj ycjs)))) in