src/Pure/type_infer.ML
changeset 5634 7f61a83d4a01
parent 4957 30c49821e61f
child 5635 b7d6b7f66131
     1.1 --- a/src/Pure/type_infer.ML	Fri Oct 09 14:19:13 1998 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Fri Oct 09 14:36:48 1998 +0200
     1.3 @@ -330,9 +330,9 @@
     1.4            "Type error in application: " ^ why,
     1.5            "",
     1.6            str_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
     1.7 -            Pretty.str " :: ", prT T']),
     1.8 +            Pretty.str " ::", Pretty.brk 1, prT T']),
     1.9            str_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.10 -            Pretty.str " :: ", prT U']), ""];
    1.11 +            Pretty.str " ::", Pretty.brk 1, prT U']), ""];
    1.12        in raise TYPE (text, [T', U'], [t', u']) end;
    1.13  
    1.14      fun err_constraint msg bs t T U =
    1.15 @@ -343,7 +343,7 @@
    1.16            "Cannot meet type constraint:",
    1.17            "",
    1.18            str_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
    1.19 -            Pretty.str " :: ", prT T']),
    1.20 +            Pretty.str " ::", Pretty.brk 1, prT T']),
    1.21            str_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
    1.22        in raise TYPE (text, [T', U'], [t']) end;
    1.23