--- a/src/HOL/Import/shuffler.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Sep 18 18:05:37 2007 +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 [] string_of_thm;
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
+val string_of_thm = PrintMode.setmp [] string_of_thm;
+val string_of_cterm = PrintMode.setmp [] string_of_cterm;
fun mk_meta_eq th =
(case concl_of th of