diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/unify.ML	Wed Nov 21 00:36:51 2001 +0100
@@ -186,7 +186,7 @@
 
 fun test_unify_types(args as (T,U,_)) =
 let val sot = Sign.string_of_typ (!sgr);
-    fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
+    fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
     val env' = unify_types(args)
 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    env'
@@ -560,8 +560,8 @@
                               (Envir.norm_term env (rlist_abs(rbinder,t)))
             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
                           termT t];
-        in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
-  in  writeln msg;  seq pdp dpairs  end;
+        in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
+  in  tracing msg;  seq pdp dpairs  end;
 
 
 (*Unify the dpairs in the environment.
@@ -588,7 +588,7 @@
 			   (MATCH (env',dp, frigid'@flexflex), reseq)))
 	  end
 	  handle CANTUNIFY => 
-	    (if tdepth > !trace_bound then writeln"Failure node" else ();
+	    (if tdepth > !trace_bound then tracing"Failure node" else ();
 	     Seq.pull reseq));
      val dps = map (fn(t,u)=> ([],t,u)) tus
   in sgr := sg;