# HG changeset patch
# User wenzelm
# Date 1374096796 -7200
# Node ID da646aa4a3bbd21e7fa52b20ad84f9bde8501a53
# Parent  6651abced1069bdf39ba1400a2b8531f0ee8e22d
tuned message;

diff -r 6651abced106 -r da646aa4a3bb src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Jul 17 23:32:28 2013 +0200
+++ b/src/Tools/quickcheck.ML	Wed Jul 17 23:33:16 2013 +0200
@@ -398,17 +398,20 @@
 fun pretty_counterex ctxt auto NONE =
     Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
-      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a " ^
-        (if genuine then "counterexample:"
-          else "potentially spurious counterexample due to underspecified functions:")
-          ^ Config.get ctxt tag ^ "\n") ::
-        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.fbrk :: 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))));
+      (Pretty.text_fold o Pretty.fbreaks)
+        (Pretty.str (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)));
 
 
 (* Isar commands *)