src/Pure/unify.ML
changeset 12262 11ff5f47df6e
parent 12231 4a25f04bea61
child 12527 d6c91bc3e49c
     1.1 --- a/src/Pure/unify.ML	Wed Nov 21 00:35:13 2001 +0100
     1.2 +++ b/src/Pure/unify.ML	Wed Nov 21 00:36:51 2001 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  
     1.5  fun test_unify_types(args as (T,U,_)) =
     1.6  let val sot = Sign.string_of_typ (!sgr);
     1.7 -    fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
     1.8 +    fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
     1.9      val env' = unify_types(args)
    1.10  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    1.11     env'
    1.12 @@ -560,8 +560,8 @@
    1.13                                (Envir.norm_term env (rlist_abs(rbinder,t)))
    1.14              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
    1.15                            termT t];
    1.16 -        in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
    1.17 -  in  writeln msg;  seq pdp dpairs  end;
    1.18 +        in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
    1.19 +  in  tracing msg;  seq pdp dpairs  end;
    1.20  
    1.21  
    1.22  (*Unify the dpairs in the environment.
    1.23 @@ -588,7 +588,7 @@
    1.24  			   (MATCH (env',dp, frigid'@flexflex), reseq)))
    1.25  	  end
    1.26  	  handle CANTUNIFY => 
    1.27 -	    (if tdepth > !trace_bound then writeln"Failure node" else ();
    1.28 +	    (if tdepth > !trace_bound then tracing"Failure node" else ();
    1.29  	     Seq.pull reseq));
    1.30       val dps = map (fn(t,u)=> ([],t,u)) tus
    1.31    in sgr := sg;