--- a/src/Tools/quickcheck.ML Sun Jan 25 13:32:32 2015 +0100
+++ b/src/Tools/quickcheck.ML Sun Jan 25 13:56:21 2015 +0100
@@ -386,20 +386,25 @@
fun pretty_counterex ctxt auto NONE =
Pretty.para (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
| pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
- (Pretty.text_fold o Pretty.fbreaks)
- (Pretty.para (tool_name auto ^ " found a " ^
- (if genuine then "counterexample:"
- else "potentially spurious counterexample due to underspecified functions:") ^
- Config.get ctxt tag) ::
- Pretty.str "" ::
- map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
- (if null eval_terms then []
- else
- Pretty.str "" :: Pretty.str "Evaluated terms:" ::
- map (fn (t, u) =>
- Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
- Syntax.pretty_term ctxt u]) (rev eval_terms)));
+ let
+ val header =
+ Pretty.para
+ (tool_name auto ^ " found a " ^
+ (if genuine then "counterexample:"
+ else "potentially spurious counterexample due to underspecified functions:") ^
+ Config.get ctxt tag);
+ val body =
+ map (fn (s, t) =>
+ Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex);
+ in
+ Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: body)) ::
+ (if null eval_terms then []
+ else
+ [Pretty.big_list "Evaluated terms:"
+ (map (fn (t, u) =>
+ Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
+ Syntax.pretty_term ctxt u]) (rev eval_terms))]))
+ end;
(* Isar commands *)