src/Pure/type_infer.ML

       | meet (PTFree (x, S'), S) =
           if Type.subsort tsig (S', S) then ()
           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";
 
 
     (* occurs check and assigment *)
 

       Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
 
     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
         (NONE, NONE) => Type.defaultS tsig
       | (NONE, SOME S) => S
       | (SOME S, NONE) => S
       | (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;
 
 
 (* decode_types -- transform parse tree into raw term *)