src/Pure/sign.ML

--- 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