diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/unify.ML	Sun May 18 15:04:09 2008 +0200
@@ -194,7 +194,7 @@
        handle Type.TUNIFY => raise CANTUNIFY;
 
 fun test_unify_types thy (args as (T,U,_)) =
-let val str_of = Sign.string_of_typ thy;
+let val str_of = Syntax.string_of_typ_global thy;
     fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
     val env' = unify_types thy args
 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
@@ -556,7 +556,7 @@
     t is always flexible.*)
 fun print_dpairs thy msg (env,dpairs) =
   let fun pdp (rbinder,t,u) =
-        let fun termT t = Sign.pretty_term thy
+        let fun termT t = Syntax.pretty_term_global thy
                               (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
                           termT t];