--- a/src/HOL/Import/import_package.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Import/import_package.ML Sat May 17 13:54:30 2008 +0200
@@ -25,8 +25,8 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-val string_of_thm = PrintMode.setmp [] string_of_thm;
-val string_of_cterm = PrintMode.setmp [] string_of_cterm;
+val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun import_tac (thyname,thmname) =
if ! quick_and_dirty