# HG changeset patch
# User wenzelm
# Date 1422104059 -3600
# Node ID f24ac9df7ab21bb8ddfafadd1a060805097903ce
# Parent  14dd7e9acd92e8d48741463985c76cb23dbc5441
avoid newline in Pretty.str;

diff -r 14dd7e9acd92 -r f24ac9df7ab2 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Jan 23 12:37:57 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jan 24 13:54:19 2015 +0100
@@ -665,7 +665,7 @@
                    (case pretties_for_scope scope verbose of
                       [] => []
                     | pretties => pstrs " for " @ pretties) @
-                   [Pretty.str ":\n"])),
+                   [Pretty.str ":", Pretty.fbrk])),
               Pretty.indent indent_size reconstructed_model]);
          print_t (K "% SZS output end FiniteModel");
          if genuine then