--- a/src/HOL/Tools/refute.ML Mon Jun 28 15:32:24 2010 +0200
+++ b/src/HOL/Tools/refute.ML Mon Jun 28 15:32:25 2010 +0200
@@ -2234,7 +2234,7 @@
(* sanity check: every element of terms' must also be *)
(* present in terms *)
val _ =
- if List.all (member (op =) terms) terms' then ()
+ if forall (member (op =) terms) terms' then ()
else
raise REFUTE ("IDT_constructor_interpreter",
"element has disappeared")
@@ -2957,7 +2957,7 @@
(* "lfp(f) == Inter({u. f(u) <= u})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
- List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
+ forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
(subs ~~ sups)
| is_subset (_, _) =
raise REFUTE ("lfp_interpreter",
@@ -3012,7 +3012,7 @@
(* "gfp(f) == Union({u. u <= f(u)})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
- List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
+ forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
(subs ~~ sups)
| is_subset (_, _) =
raise REFUTE ("gfp_interpreter",