1.1 --- a/src/Pure/unify.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/unify.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4         handle Type.TUNIFY => raise CANTUNIFY;
     1.5  
     1.6  fun test_unify_types thy (args as (T,U,_)) =
     1.7 -let val str_of = Sign.string_of_typ thy;
     1.8 +let val str_of = Syntax.string_of_typ_global thy;
     1.9      fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
    1.10      val env' = unify_types thy args
    1.11  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    1.12 @@ -556,7 +556,7 @@
    1.13      t is always flexible.*)
    1.14  fun print_dpairs thy msg (env,dpairs) =
    1.15    let fun pdp (rbinder,t,u) =
    1.16 -        let fun termT t = Sign.pretty_term thy
    1.17 +        let fun termT t = Syntax.pretty_term_global thy
    1.18                                (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
    1.19              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
    1.20                            termT t];