# HG changeset patch
# User paulson
# Date 818414726 -3600
# Node ID 893e8d93a54c9c4ff331731a5fccf3f9c73dd0d8
# Parent  bf523422a3dffe2577e302a30a8163cc2e8bd629
type_of1: improved error messages

diff -r bf523422a3df -r 893e8d93a54c src/Pure/term.ML
--- 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);