src/Pure/unify.ML

        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise CANTUNIFY;
 
 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'
 end;
 

   let fun pdp (rbinder,t,u) =
         let fun termT t = Sign.pretty_term (!sgr)
                               (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.
   Returns flex-flex disagreement pairs NOT IN normal form. 
   SIMPL may raise exception CANTUNIFY. *)

 		 else ();
 		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
 			   (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;
      add_unify 1 ((env,dps), Seq.empty) 
   end;