diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/type.ML	Mon Jan 29 14:16:13 1996 +0100
@@ -904,7 +904,7 @@
                 val (T, tyeT) = inf(Ts, f, tyeU);
                 fun err s =
                   raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
-                val msg = "function type is incompatible with argument type"
+		val msg = "function type is incompatible with argument type"
             in case T of
                  Type("fun", [T1, T2]) =>
                    ( (T2, unify1 tsig ((T1, U), tyeT))
@@ -1049,7 +1049,7 @@
 
 
 (*Infer types for terms.  Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that
-        the type of ti unifies with Ti (i=1,...,n).
+	the type of ti unifies with Ti (i=1,...,n).
   types is a partial map from indexnames to types (constrains Free, Var).
   sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   used is the list of already used type variables.