src/Pure/sign.ML
changeset 39137 ccb53edd59f0
parent 39133 70d3915c92f0
child 39289 92b50c8bb67b
     1.1 --- a/src/Pure/sign.ML	Sun Sep 05 22:23:48 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Sep 05 23:16:21 2010 +0200
     1.3 @@ -270,8 +270,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 msg = cat_lines
     1.8 -          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
     1.9 +        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
    1.10        in raise TYPE (msg, [T, U], [t', u']) end;
    1.11  
    1.12      fun typ_of (_, Const (_, T)) = T