Term.string_of_vname;

--- 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"

--- a/src/Pure/Isar/locale.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -2133,7 +2133,7 @@
       |> fold Term.add_varnames all_vs
     val _ = if null vars then ()
          else error ("Illegal schematic variable(s) in instantiation: " ^
-           commas_quote (map Syntax.string_of_vname vars));
+           commas_quote (map Term.string_of_vname vars));
     (* replace new types (which are TFrees) by ones with new names *)
     val new_Tnames = map fst (fold Term.add_tfrees all_vs [])
       |> Name.names (Name.make_context used) "'a"

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -460,7 +460,7 @@
   Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt);
 
 fun reject_schematic (Var (xi, _)) =
-      error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)
+      error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
   | reject_schematic (Abs (_, _, t)) = reject_schematic t
   | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
   | reject_schematic _ = ();

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -78,7 +78,7 @@
       (case try Name.dest_skolem x of
         NONE => tagit var_tag s
       | SOME x' => tagit skolem_tag
-          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
+          (setmp show_question_marks true Term.string_of_vname (x', i)))
   | NONE => tagit var_tag s);
 
 val proof_general_trans =

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -89,7 +89,7 @@
       (case try Name.dest_skolem x of
         NONE => tagit var_tag s
       | SOME x' => tagit skolem_tag
-          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
+          (setmp show_question_marks true Term.string_of_vname (x', i)))
   | NONE => tagit var_tag s);
 
 val proof_general_trans =

--- a/src/Pure/envir.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/envir.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -74,7 +74,7 @@
   in  (env',v)  end;
 
 fun var_clash ixn T T' = raise TYPE ("Variable " ^
-  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
+  quote (Term.string_of_vname ixn) ^ " has two distinct types",
   [T', T], []);
 
 fun gen_lookup f asol (xname, T) =

--- a/src/Pure/pattern.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/pattern.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -71,7 +71,7 @@
 
 fun proj_fail thy (env,binders,F,_,is,t) =
   if !trace_unify_fail
-  then let val f = Syntax.string_of_vname F
+  then let val f = Term.string_of_vname F
            val xs = bnames binders is
            val u = string_of_term thy env binders t
            val ys = bnames binders (subtract (op =) is (loose_bnos t))
@@ -83,7 +83,7 @@
 
 fun ocheck_fail thy (F,t,binders,env) =
   if !trace_unify_fail
-  then let val f = Syntax.string_of_vname F
+  then let val f = Term.string_of_vname F
            val u = string_of_term thy env binders t
        in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
                   "\nCannot unify!\n")

--- a/src/Pure/type_infer.ML	Sat Apr 14 17:36:03 2007 +0200
+++ b/src/Pure/type_infer.ML	Sat Apr 14 17:36:05 2007 +0200
@@ -273,7 +273,7 @@
           else raise NO_UNIFIER (not_of_sort x S' S)
       | meet (PTVar (xi, S'), S) =
           if Type.subsort tsig (S', S) then ()
-          else raise NO_UNIFIER (not_of_sort (Syntax.string_of_vname xi) S' S)
+          else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S)
       | meet (Param _, _) = sys_error "meet";
 
 
@@ -456,7 +456,7 @@
     val env = distinct eq (map (apsnd map_sort) raw_env);
     val _ = (case duplicates (eq_fst (op =)) env of [] => ()
       | dups => error ("Inconsistent sort constraints for type variable(s) "
-          ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
+          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
 
     fun get xi =
       (case (AList.lookup (op =) env xi, def_sort xi) of
@@ -466,7 +466,7 @@
       | (SOME S, SOME S') =>
           if Type.eq_sort tsig (S, S') then S'
           else error ("Sort constraint inconsistent with default for type variable " ^
-            quote (Syntax.string_of_vname' xi)));
+            quote (Term.string_of_vname' xi)));
   in get end;