# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 27cca5416a88a391e9eae5cd990c712e80112237
# Parent  42fed8eac357c0a5036f05d82baea653bb3ce231
Adopted output of values command

diff -r 42fed8eac357 -r 27cca5416a88 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -2552,8 +2552,9 @@
     val (ts, _) = Predicate.yieldn k ts;
     val setT = HOLogic.mk_setT T;
     val elemsT = HOLogic.mk_set T ts;
+    val cont = Free ("...", setT)
   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 Set.union}, setT --> setT --> setT) $ elemsT $ cont
   end;
   (*
 fun random_values ctxt k t =