src/HOL/ex/predicate_compile.ML
changeset 32683 7c1fe854ca6a
parent 32351 96f9e6402403
child 32701 5059a733a4b8
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -2152,7 +2152,7 @@
     1.4      val (ts, _) = Predicate.yieldn k t;
     1.5      val elemsT = HOLogic.mk_set T ts;
     1.6    in if k = ~1 orelse length ts < k then elemsT
     1.7 -    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
     1.8 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
     1.9    end;
    1.10  
    1.11  fun values_cmd modes k raw_t state =