avoid direct access to print_mode;

--- 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

--- a/src/HOL/Tools/res_atp.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -946,7 +946,7 @@
       val ctxt = ProofContext.init (theory_of_thm th)
   in  isar_atp (ctxt, [], th)  end;
 
-val isar_atp_writeonly = setmp print_mode []
+val isar_atp_writeonly = PrintMode.with_default
       (fn (ctxt, chain_ths, th) =>
        if Thm.no_prems th then ()
        else

--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -19,8 +19,8 @@
 structure IoaPackage: IOA_PACKAGE =
 struct
 
-val string_of_typ = setmp print_mode [] o Sign.string_of_typ;
-val string_of_term = setmp print_mode [] o Sign.string_of_term;
+val string_of_typ = PrintMode.with_default o Sign.string_of_typ;
+val string_of_term = PrintMode.with_default o Sign.string_of_term;
 
 exception malformed;
 

--- a/src/Pure/General/markup.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/General/markup.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -170,7 +170,7 @@
   fun add_mode name output = CRITICAL (fn () =>
     change modes (Symtab.update_new (name, {output = output})));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
+    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
 fun output ("", _) = ("", "")

--- a/src/Pure/General/output.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -67,7 +67,7 @@
   fun add_mode name output escape = CRITICAL (fn () =>
     change modes (Symtab.update_new (name, {output = output, escape = escape})));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
+    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
 fun output_width x = #output (get_mode ()) x;

--- a/src/Pure/General/pretty.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -93,7 +93,7 @@
   fun add_mode name indent = CRITICAL (fn () =>
     change modes (Symtab.update_new (name, {indent = indent})));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
+    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
 fun mode_indent x y = #indent (get_mode ()) x y;

--- a/src/Pure/Isar/proof_context.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -314,7 +314,7 @@
     val consts = consts_of ctxt;
     val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs");
     val t' = t
-      |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (! print_mode @ [""]))
+      |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (print_mode_value () @ [""]))
       |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [Syntax.internalM])
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;

--- a/src/Pure/Isar/session.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/Isar/session.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -87,7 +87,7 @@
       Secure.use_noncritical root;
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
-    |> setmp_noncritical print_mode (modes @ ! print_mode)
+    |> setmp_noncritical print_mode (modes @ print_mode_value ())
     |> setmp_noncritical Multithreading.trace trace_threads
     |> setmp_noncritical Multithreading.max_threads
       (if Multithreading.available then max_threads

--- a/src/Pure/Syntax/printer.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -367,14 +367,14 @@
 (* pretty_term_ast *)
 
 fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
-  pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
+  pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
     trf tokentrf false curried ast 0;
 
 
 (* pretty_typ_ast *)
 
 fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
-  pretty I ctxt (mode_tabs prtabs (! print_mode))
+  pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
     trf tokentrf true false ast 0;
 
 end;

--- a/src/Tools/nbe.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Tools/nbe.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -373,7 +373,7 @@
     val ct = Thm.cterm_of thy t;
     val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
     val ty = Term.type_of t';
-    val p = Library.setmp print_mode (modes @ ! print_mode) (fn () =>
+    val p = Library.setmp print_mode (modes @ print_mode_value ()) (fn () =>
       Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
   in Pretty.writeln p end;