Inserted spaces in error messages to improve readability
authorpaulson
Fri, 26 Jul 1996 12:27:22 +0200
changeset 1890 a525e960f2bd
parent 1889 661603db8ee2
child 1891 618f48bd4532
Inserted spaces in error messages to improve readability
src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jul 26 12:26:32 1996 +0200
+++ b/src/Pure/sign.ML	Fri Jul 26 12:27:22 1996 +0200
@@ -229,7 +229,7 @@
            Some(S') => if S=S' then tvars
                        else raise_type
                             ("Type variable "^Syntax.string_of_vname a^
-                             "has two distinct sorts") [TVar(a,S'),T] []
+                             " has two distinct sorts") [TVar(a,S'),T] []
          | None => v::tvars));
 
 (* check for duplicate Vars with distinct types *)
@@ -242,7 +242,7 @@
                Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
                            else raise_type
                              ("Variable "^Syntax.string_of_vname ixn^
-                              "has two distinct types") [T',T] []
+                              " has two distinct types") [T',T] []
              | None => (v::vars,tvars))
         | Bound _ => (vars,tvars)
         | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t