diff -r 621ac078f7b0 -r 397ce0940c44 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Jan 25 13:56:21 2015 +0100
+++ b/src/Tools/quickcheck.ML	Sun Jan 25 15:40:28 2015 +0100
@@ -393,11 +393,10 @@
               (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);
+        fun pretty_cex (x, t) =
+          Pretty.block [Pretty.str (x ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t];
       in
-        Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: body)) ::
+        Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: map pretty_cex (rev cex))) ::
           (if null eval_terms then []
            else
             [Pretty.big_list "Evaluated terms:"