avoid newline in Pretty.str;
authorwenzelm
Sat Jan 24 13:54:19 2015 +0100 (2015-01-24 ago)
changeset 59429f24ac9df7ab2
parent 59428 14dd7e9acd92
child 59430 b65809f05dc9
avoid newline in Pretty.str;
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Jan 23 12:37:57 2015 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jan 24 13:54:19 2015 +0100
     1.3 @@ -665,7 +665,7 @@
     1.4                     (case pretties_for_scope scope verbose of
     1.5                        [] => []
     1.6                      | pretties => pstrs " for " @ pretties) @
     1.7 -                   [Pretty.str ":\n"])),
     1.8 +                   [Pretty.str ":", Pretty.fbrk])),
     1.9                Pretty.indent indent_size reconstructed_model]);
    1.10           print_t (K "% SZS output end FiniteModel");
    1.11           if genuine then