# HG changeset patch
# User nipkow
# Date 907936608 -7200
# Node ID 7f61a83d4a01c0e5015ea33c4ad81bb5bfe9f9b8
# Parent  fb7fa1b154c4980003ed2a607c87e5effd1d1bd4
More pretty breaks in error msgs.

diff -r fb7fa1b154c4 -r 7f61a83d4a01 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Oct 09 14:19:13 1998 +0200
+++ b/src/Pure/type_infer.ML	Fri Oct 09 14:36:48 1998 +0200
@@ -330,9 +330,9 @@
           "Type error in application: " ^ why,
           "",
           str_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
-            Pretty.str " :: ", prT T']),
+            Pretty.str " ::", Pretty.brk 1, prT T']),
           str_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
-            Pretty.str " :: ", prT U']), ""];
+            Pretty.str " ::", Pretty.brk 1, prT U']), ""];
       in raise TYPE (text, [T', U'], [t', u']) end;
 
     fun err_constraint msg bs t T U =
@@ -343,7 +343,7 @@
           "Cannot meet type constraint:",
           "",
           str_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
-            Pretty.str " :: ", prT T']),
+            Pretty.str " ::", Pretty.brk 1, prT T']),
           str_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
       in raise TYPE (text, [T', U'], [t']) end;