Added a few breaks in error text.
authornipkow
Fri, 09 Oct 1998 14:19:13 +0200
changeset 5633 fb7fa1b154c4
parent 5632 5682dce02591
child 5634 7f61a83d4a01
Added a few breaks in error text.
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