# HG changeset patch
# User wenzelm
# Date 861296701 -7200
# Node ID 98ad57d99427975f4526c45dbb9cfbf4d8b0063e
# Parent  db6941221197bf1c016dd590010a28ab3a365b86
tuned error msgs;

diff -r db6941221197 -r 98ad57d99427 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Apr 17 18:46:58 1997 +0200
+++ b/src/Pure/type_infer.ML	Thu Apr 17 19:05:01 1997 +0200
@@ -340,11 +340,11 @@
          [unif_failed msg,
           "Type error in application:",
           "",
-          str_of (Pretty.block [Pretty.str "operator:     ", Pretty.brk 1, prt t',
+          str_of (Pretty.block [Pretty.str "operator:", Pretty.brk 2, prt t',
             Pretty.str " :: ", prT T']),
-          str_of (Pretty.block [Pretty.str "expected type:", Pretty.brk 1, prT U_to_V']),
+          str_of (Pretty.block [Pretty.str "expected:", Pretty.brk 2, prT U_to_V']),
           "",
-          str_of (Pretty.block [Pretty.str "operand:      ", Pretty.brk 1, prt u',
+          str_of (Pretty.block [Pretty.str "operand:", Pretty.brk 3, prt u',
             Pretty.str " :: ", prT U']), ""];
       in raise_type text [T', U_to_V', U'] [t', u'] end;
 
@@ -355,9 +355,9 @@
          [unif_failed msg,
           "Cannot meet type constraint:",
           "",
-          str_of (Pretty.block [Pretty.str "term:          ", Pretty.brk 1, prt t',
+          str_of (Pretty.block [Pretty.str "term:", Pretty.brk 2, prt t',
             Pretty.str " :: ", prT T']),
-          str_of (Pretty.block [Pretty.str "expected type: ", Pretty.brk 1, prT U']), ""];
+          str_of (Pretty.block [Pretty.str "type:", Pretty.brk 2, prT U']), ""];
       in raise_type text [T', U'] [t'] end;