Added a few breaks in error text.
--- 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