src/Pure/type_infer.ML

         val text = cat_lines
          [unif_failed msg,
           "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 =
       let
         val ([t'], [T', U']) = prep_output bs [t] [T, U];
         val text = cat_lines
          [unif_failed msg,
           "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;
 
 
     (* main *)