changeset 39137 | ccb53edd59f0 |
parent 39133 | 70d3915c92f0 |
child 39289 | 92b50c8bb67b |
--- a/src/Pure/sign.ML Sun Sep 05 22:23:48 2010 +0200 +++ b/src/Pure/sign.ML Sun Sep 05 23:16:21 2010 +0200 @@ -270,8 +270,7 @@ val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); - val msg = cat_lines - (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U); + val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U); in raise TYPE (msg, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T