--- a/src/Pure/term.ML Fri Dec 08 10:23:29 1995 +0100
+++ b/src/Pure/term.ML Fri Dec 08 10:25:26 1995 +0100
@@ -129,9 +129,10 @@
in case T of
Type("fun",[T1,T2]) =>
if T1=U then T2 else raise TYPE
- ("type_of: type mismatch in application", [T1,U], [f$u])
- | _ => raise TYPE ("type_of: Rator must have function type",
- [T,U], [f$u])
+ ("type_of: type mismatch in application", [T1,U], [f$u])
+ | _ => raise TYPE
+ ("type_of: function type is expected in application",
+ [T,U], [f$u])
end;
fun type_of t : typ = type_of1 ([],t);