Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 25 Jan 2015 15:40:28 +0100
changeset 59439 397ce0940c44
parent 59438 621ac078f7b0
child 59440 07e3c15cb10c
tuned;
src/Tools/quickcheck.ML file | annotate | diff | comparison | revisions 
--- 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:"
isabelle