diff -r b11a9beabe7d -r 23963361278c src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Provers/blast.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -1212,7 +1212,7 @@
                      | SOME(v,is) => if is=bounds ts then Var v
                             else raise TRANS
                                 ("Discrepancy among occurrences of "
-                                 ^ Syntax.string_of_vname ix))
+                                 ^ Term.string_of_vname ix))
             | Term.Abs (a,_,body) =>
                   if null ts then Abs(a, from (lev+1) body)
                   else raise TRANS "argument not in normal form"