src/HOL/ex/predicate_compile.ML

--- a/src/HOL/ex/predicate_compile.ML	Fri Sep 18 14:09:38 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Sat Sep 19 07:38:03 2009 +0200
@@ -2152,7 +2152,7 @@
     val (ts, _) = Predicate.yieldn k t;
     val elemsT = HOLogic.mk_set T ts;
   in if k = ~1 orelse length ts < k then elemsT
-    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
   end;
 
 fun values_cmd modes k raw_t state =