tuned nitpick message: more like quickcheck;
authorwenzelm
Fri, 25 Sep 2020 15:40:35 +0200
changeset 72298 a540283d6b58
parent 72297 bc31c4a2c77c
child 72299 0c7a74a1c6d9
tuned nitpick message: more like quickcheck;
src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 25 14:40:50 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 25 15:40:35 2020 +0200
@@ -657,7 +657,7 @@
                    (case pretties_for_scope scope verbose of
                       [] => []
                     | pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @
-                   [Pretty.str ":", Pretty.fbrk])),
+                   [Pretty.str ":"])),
               Pretty.indent indent_size reconstructed_model]);
          print_t (K "% SZS output end FiniteModel");
          if genuine then