src/Pure/sign.ML
changeset 39289 92b50c8bb67b
parent 39137 ccb53edd59f0
child 39290 44e4d8dfd6bf
     1.1 --- a/src/Pure/sign.ML	Sun Sep 12 19:04:02 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Sep 12 19:55:45 2010 +0200
     1.3 @@ -265,12 +265,12 @@
     1.4  
     1.5  fun type_check pp tm =
     1.6    let
     1.7 -    fun err_appl why bs t T u U =
     1.8 +    fun err_appl bs t T u U =
     1.9        let
    1.10          val xs = map Free bs;           (*we do not rename here*)
    1.11          val t' = subst_bounds (xs, t);
    1.12          val u' = subst_bounds (xs, u);
    1.13 -        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
    1.14 +        val msg = Type.appl_error pp t' T u' U;
    1.15        in raise TYPE (msg, [T, U], [t', u']) end;
    1.16  
    1.17      fun typ_of (_, Const (_, T)) = T
    1.18 @@ -283,8 +283,8 @@
    1.19            let val T = typ_of (bs, t) and U = typ_of (bs, u) in
    1.20              (case T of
    1.21                Type ("fun", [T1, T2]) =>
    1.22 -                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
    1.23 -            | _ => err_appl "Operator not of function type" bs t T u U)
    1.24 +                if T1 = U then T2 else err_appl bs t T u U
    1.25 +            | _ => err_appl bs t T u U)
    1.26            end;
    1.27    in typ_of ([], tm) end;
    1.28