# 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 =