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

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

     3.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Sep 17 16:06:35 2007 +0200
     3.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Sep 17 16:36:41 2007 +0200
     3.3 @@ -19,8 +19,8 @@
     3.4  structure IoaPackage: IOA_PACKAGE =
     3.5  struct
     3.6  
     3.7 -val string_of_typ = setmp print_mode [] o Sign.string_of_typ;
     3.8 -val string_of_term = setmp print_mode [] o Sign.string_of_term;
     3.9 +val string_of_typ = PrintMode.with_default o Sign.string_of_typ;
    3.10 +val string_of_term = PrintMode.with_default o Sign.string_of_term;
    3.11  
    3.12  exception malformed;
    3.13  

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

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

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

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

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

     9.1 --- a/src/Pure/Syntax/printer.ML	Mon Sep 17 16:06:35 2007 +0200
     9.2 +++ b/src/Pure/Syntax/printer.ML	Mon Sep 17 16:36:41 2007 +0200
     9.3 @@ -367,14 +367,14 @@
     9.4  (* pretty_term_ast *)
     9.5  
     9.6  fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
     9.7 -  pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
     9.8 +  pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
     9.9      trf tokentrf false curried ast 0;
    9.10  
    9.11  
    9.12  (* pretty_typ_ast *)
    9.13  
    9.14  fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
    9.15 -  pretty I ctxt (mode_tabs prtabs (! print_mode))
    9.16 +  pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
    9.17      trf tokentrf true false ast 0;
    9.18  
    9.19  end;

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