src/HOL/Tools/Nitpick/nitpick.ML
changeset 72298 a540283d6b58
parent 72205 bc71db05abe3
child 72327 da2cbe54e53e
--- 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