--- 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];