# HG changeset patch
# User wenzelm
# Date 1422190581 -3600
# Node ID 621ac078f7b0df048ec5794ff42d1ebe037c1052
# Parent  2c8f889254655ed39ff67d82a232c93b85f2a8cb
more compact message;

diff -r 2c8f88925465 -r 621ac078f7b0 src/Tools/quickcheck.ML
--- 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 *)