diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Sun May 18 15:04:09 2008 +0200
@@ -166,9 +166,9 @@
     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