src/Provers/blast.ML

   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
                                else Term.Abs(a, dummyT, showTerm (d-1) t)
   | 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). *)
 fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
   | negOfGoal G = G;

   let val t' = norm (negOfGoal t)
       val stm = string_of thy 8 t'
   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;
 
 
 (*Print tracing information at each iteration of prover*)
 fun tracing (State {thy, fullTrace, ...}) brs =