--- a/src/HOL/Import/shuffler.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Import/shuffler.ML Sat May 29 14:57:39 2004 +0200
@@ -58,10 +58,8 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = Library.setmp print_mode [] string_of_thm
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm
-
-val commafy = String.concat o separate ", "
+val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
+val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
fun mk_meta_eq th =
(case concl_of th of