# HG changeset patch
# User haftmann
# Date 1277731945 -7200
# Node ID 6e89e103f7c7091c3f005b96cad2f72c916587fc
# Parent  501b0cae5aa806e5fd4dd17b01d09e3e23c94342
avoid List.all

diff -r 501b0cae5aa8 -r 6e89e103f7c7 src/HOL/Tools/refute.ML
--- 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",