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