1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 01 08:07:27 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 01 08:07:28 2011 +0200
     1.3 @@ -1896,13 +1896,15 @@
     1.4       handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
     1.5    in ((T, ts), statistics) end;
     1.6  
     1.7 -fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
     1.8 +fun values param_user_modes ((raw_expected, stats), comp_options) k t_compr ctxt =
     1.9    let
    1.10      val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
    1.11      val setT = HOLogic.mk_setT T
    1.12      val elems = HOLogic.mk_set T ts
    1.13 -    val cont = Free ("dots", setT)  (* FIXME proper name!? *)
    1.14 +    val ([dots], ctxt') =
    1.15 +      Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix ("...", [], 1000))] ctxt 
    1.16      (* check expected values *)
    1.17 +    val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
    1.18      val () =
    1.19        case raw_expected of
    1.20          NONE => ()
    1.21 @@ -1913,17 +1915,16 @@
    1.22              "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
    1.23              "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
    1.24    in
    1.25 -    (if k = ~1 orelse length ts < k then elems
    1.26 -    else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont, statistics)
    1.27 +    ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics), ctxt')
    1.28    end;
    1.29  
    1.30  fun values_cmd print_modes param_user_modes options k raw_t state =
    1.31    let
    1.32      val ctxt = Toplevel.context_of state
    1.33      val t = Syntax.read_term ctxt raw_t
    1.34 -    val (t', stats) = values ctxt param_user_modes options k t
    1.35 +    val ((t', stats), ctxt') = values param_user_modes options k t ctxt
    1.36      val ty' = Term.type_of t'
    1.37 -    val ctxt' = Variable.auto_fixes t' ctxt
    1.38 +    val ctxt'' = Variable.auto_fixes t' ctxt'
    1.39      val pretty_stat =
    1.40        case stats of
    1.41            NONE => []
    1.42 @@ -1940,8 +1941,8 @@
    1.43               @ maps pretty_entry xs
    1.44            end
    1.45      val p = Print_Mode.with_modes print_modes (fn () =>
    1.46 -      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    1.47 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
    1.48 +      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt'' t'), Pretty.fbrk,
    1.49 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt'' ty')]
    1.50          @ pretty_stat)) ();
    1.51    in Pretty.writeln p end;
    1.52