tuned error msgs;
authorwenzelm
Thu Apr 17 19:05:01 1997 +0200 (1997-04-17)
changeset 298098ad57d99427
parent 2979 db6941221197
child 2981 aa5aeb6467c6
tuned error msgs;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Thu Apr 17 18:46:58 1997 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Apr 17 19:05:01 1997 +0200
     1.3 @@ -340,11 +340,11 @@
     1.4           [unif_failed msg,
     1.5            "Type error in application:",
     1.6            "",
     1.7 -          str_of (Pretty.block [Pretty.str "operator:     ", Pretty.brk 1, prt t',
     1.8 +          str_of (Pretty.block [Pretty.str "operator:", Pretty.brk 2, prt t',
     1.9              Pretty.str " :: ", prT T']),
    1.10 -          str_of (Pretty.block [Pretty.str "expected type:", Pretty.brk 1, prT U_to_V']),
    1.11 +          str_of (Pretty.block [Pretty.str "expected:", Pretty.brk 2, prT U_to_V']),
    1.12            "",
    1.13 -          str_of (Pretty.block [Pretty.str "operand:      ", Pretty.brk 1, prt u',
    1.14 +          str_of (Pretty.block [Pretty.str "operand:", Pretty.brk 3, prt u',
    1.15              Pretty.str " :: ", prT U']), ""];
    1.16        in raise_type text [T', U_to_V', U'] [t', u'] end;
    1.17  
    1.18 @@ -355,9 +355,9 @@
    1.19           [unif_failed msg,
    1.20            "Cannot meet type constraint:",
    1.21            "",
    1.22 -          str_of (Pretty.block [Pretty.str "term:          ", Pretty.brk 1, prt t',
    1.23 +          str_of (Pretty.block [Pretty.str "term:", Pretty.brk 2, prt t',
    1.24              Pretty.str " :: ", prT T']),
    1.25 -          str_of (Pretty.block [Pretty.str "expected type: ", Pretty.brk 1, prT U']), ""];
    1.26 +          str_of (Pretty.block [Pretty.str "type:", Pretty.brk 2, prT U']), ""];
    1.27        in raise_type text [T', U'] [t'] end;
    1.28  
    1.29