# HG changeset patch
# User nipkow
# Date 907935553 -7200
# Node ID fb7fa1b154c4980003ed2a607c87e5effd1d1bd4
# Parent  5682dce0259161288cd19f1c0ddacce1757e2aa5
Added a few breaks in error text.

diff -r 5682dce02591 -r fb7fa1b154c4 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Oct 09 11:27:11 1998 +0200
+++ b/src/Pure/sign.ML	Fri Oct 09 14:19:13 1998 +0200
@@ -605,10 +605,12 @@
         val text = cat_lines
          ["Type error in application: " ^ why,
           "",
-          Pretty.string_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
-            Pretty.str " :: ", prT T]),
-          Pretty.string_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
-            Pretty.str " :: ", prT U]), ""];
+          Pretty.string_of
+           (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
+                          Pretty.str " ::", Pretty.brk 1, prT T]),
+          Pretty.string_of
+           (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
+                          Pretty.str " ::", Pretty.brk 1, prT U]), ""];
       in raise TYPE (text, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T