diff -r d5883907c514 -r 8408edac8f6b src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -165,9 +165,10 @@
   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: " ^ Display.raw_string_of_term rator ^
-                    " expected " ^
-                    Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term 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))
     end;
 
 (*Instantiate constant c with the supplied types, but if they don't match its declared