--- a/src/HOL/Import/import_package.ML Mon Sep 17 16:06:35 2007 +0200
+++ b/src/HOL/Import/import_package.ML Mon Sep 17 16:36:41 2007 +0200
@@ -25,8 +25,8 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-val string_of_thm = Library.setmp print_mode [] string_of_thm;
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
+val string_of_thm = PrintMode.with_default string_of_thm;
+val string_of_cterm = PrintMode.with_default string_of_cterm;
fun import_tac (thyname,thmname) =
if ! quick_and_dirty