# HG changeset patch
# User wenzelm
# Date 1085986403 -7200
# Node ID 83f1dc18f1f1524a2eb3260cd2fed816dc1edd42
# Parent  44d92c12b255d8b295d5d566d2131f97094bb6b2
oops -- no Output.out here;

diff -r 44d92c12b255 -r 83f1dc18f1f1 src/HOL/Import/import_package.ML
--- 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
diff -r 44d92c12b255 -r 83f1dc18f1f1 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat May 29 16:50:53 2004 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon May 31 08:53:23 2004 +0200
@@ -58,8 +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 [] (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 mk_meta_eq th =
     (case concl_of th of