src/Pure/sign.ML
changeset 5635 b7d6b7f66131
parent 5633 fb7fa1b154c4
child 5642 1b3e48bdbb93
     1.1 --- a/src/Pure/sign.ML	Fri Oct 09 14:36:48 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 09 15:28:04 1998 +0200
     1.3 @@ -602,15 +602,7 @@
     1.4          val xs = map Free bs;		(*we do not rename here*)
     1.5          val t' = subst_bounds (xs, t);
     1.6          val u' = subst_bounds (xs, u);
     1.7 -        val text = cat_lines
     1.8 -         ["Type error in application: " ^ why,
     1.9 -          "",
    1.10 -          Pretty.string_of
    1.11 -           (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    1.12 -                          Pretty.str " ::", Pretty.brk 1, prT T]),
    1.13 -          Pretty.string_of
    1.14 -           (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.15 -                          Pretty.str " ::", Pretty.brk 1, prT U]), ""];
    1.16 +        val text = cat_lines(TypeInfer.appl_error prt prT why t' T u' U);
    1.17        in raise TYPE (text, [T, U], [t', u']) end;
    1.18  
    1.19      fun typ_of (_, Const (_, T)) = T