--- a/src/HOL/Import/import_package.ML Sat May 29 16:50:53 2004 +0200
+++ b/src/HOL/Import/import_package.ML Mon May 31 08:53:23 2004 +0200
@@ -30,8 +30,8 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-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);
+val string_of_thm = Library.setmp print_mode [] string_of_thm;
+val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
fun import_tac (thyname,thmname) =
if !SkipProof.quick_and_dirty