diff -r 64e850c3da9e -r 1035c89b4c02 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Provers/blast.ML	Sun May 18 15:04:09 2008 +0200
@@ -614,7 +614,7 @@
   | showTerm d (f $ u)       = if d=0 then dummyVar
                                else Term.$ (showTerm d f, showTerm (d-1) u);
 
-fun string_of thy d t = Sign.string_of_term thy (showTerm d t);
+fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
 
 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   Ex(P) is duplicated as the assumption ~Ex(P). *)
@@ -638,7 +638,7 @@
   in
       case topType thy t' of
           NONE   => stm   (*no type to attach*)
-        | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ thy T
+        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
   end;