src/HOL/Tools/metis_tools.ML

 
   fun apply_list rator nargs rands =
     let val trands = terms_of rands
     in  if length trands = nargs then Term (list_comb(rator, trands))
         else error
-          ("apply_list: wrong number of arguments: " ^ Sign.string_of_term CPure.thy rator ^
-            " expected " ^
-            Int.toString nargs ^ " received " ^ commas (map (Sign.string_of_term CPure.thy) trands))
+          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global CPure.thy rator ^
+            " expected " ^ Int.toString nargs ^
+            " received " ^ commas (map (Syntax.string_of_term_global CPure.thy) trands))
     end;
 
 (*Instantiate constant c with the supplied types, but if they don't match its declared
   sort constraints, replace by a general type.*)
 fun const_of ctxt (c,Ts) =  Const (c, dummyT)