# HG changeset patch
# User wenzelm
# Date 1283715684 -7200
# Node ID 917b4b6ba3d2110651758c6e3936bd655ec1a270
# Parent  70d3915c92f09ed85ef9f45aac5e0fb13c6ce81a
turned show_sorts/show_types into proper configuration options;

diff -r 70d3915c92f0 -r 917b4b6ba3d2 NEWS
--- a/NEWS	Sun Sep 05 19:47:40 2010 +0200
+++ b/NEWS	Sun Sep 05 21:41:24 2010 +0200
@@ -31,6 +31,8 @@
   ML (Config.T)                 Isar (attribute)
 
   eta_contract                  eta_contract
+  show_sorts                    show_sorts
+  show_types                    show_types
   show_question_marks           show_question_marks
   show_consts                   show_consts
 
diff -r 70d3915c92f0 -r 917b4b6ba3d2 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 19:47:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 21:41:24 2010 +0200
@@ -96,8 +96,8 @@
 
 text {*
   \begin{mldecls} 
-    @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
+    @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
     @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
diff -r 70d3915c92f0 -r 917b4b6ba3d2 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 19:47:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 21:41:24 2010 +0200
@@ -118,8 +118,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls} 
-    \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Groups.thy	Sun Sep 05 21:41:24 2010 +0200
@@ -124,11 +124,11 @@
 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
 
-typed_print_translation {*
+typed_print_translation (advanced) {*
 let
-  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
-    if (not o null) ts orelse T = dummyT
-      orelse not (! show_types) andalso can Term.dest_Type T
+  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
+    if not (null ts) orelse T = dummyT
+      orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
     then raise Match
     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -191,6 +191,7 @@
     let
         val ctxt = ctxt0
           |> Config.put show_all_types true
+          |> Config.put show_sorts true
           |> Config.put Syntax.ambiguity_enabled true;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
@@ -199,8 +200,7 @@
     in
         quote (
         Print_Mode.setmp [] (
-        setmp_CRITICAL show_brackets false (
-        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
+        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
         ct)
     end
 
@@ -214,7 +214,7 @@
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
                    handle TERM _ => ct
         fun match u = t aconv u
-        fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
+        fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
           | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
           | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
           | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -439,8 +439,8 @@
       in Context.mapping I upd_prf ctxt end;
 
    fun string_of_typ T =
-      setmp_CRITICAL show_sorts true
-       (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+      Print_Mode.setmp []
+        (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -288,7 +288,7 @@
       Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
       orelse error (cat_lines
       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
-       setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
 
     val _ = map check_sorts fixes
   in
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -281,7 +281,8 @@
 
 fun set_show_all_types ctxt =
   Config.put show_all_types
-    (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
+    (Config.get ctxt show_types orelse Config.get ctxt show_sorts
+      orelse Config.get ctxt show_all_types) ctxt
 
 val indent_size = 2
 
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -947,11 +947,12 @@
 
 fun string_for_proof ctxt0 full_types i n =
   let
-    val ctxt = Config.put show_free_types false ctxt0
+    val ctxt = ctxt0
+      |> Config.put show_free_types false
+      |> Config.put show_types true
     fun fix_print_mode f x =
-      setmp_CRITICAL show_types true
-           (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                                     (print_mode_value ())) f) x
+      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                               (print_mode_value ())) f x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -69,15 +69,15 @@
 
 in
 
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
+fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
       let val t' =
-        if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
+        if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
         else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
       in list_comb (t', ts) end
-  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
+  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
       if T = dummyT then list_comb (syntax_numeral t, ts)
       else raise Match
-  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
+  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
 
 end;
 
@@ -86,6 +86,6 @@
 
 val setup =
   Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
-  Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
+  Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
 
 end;
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/record.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -699,9 +699,9 @@
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
+                    val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
                     val alphas' =
-                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
-                        (but_last alphas);
+                      map (term_of_typ o Envir.norm_type subst o varifyT) (but_last alphas);
 
                     val more' = mk_ext rest;
                   in
@@ -810,7 +810,7 @@
     val T = decode_type thy t;
     val varifyT = varifyT (Term.maxidx_of_typ T);
 
-    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
+    val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
 
     fun strip_fields T =
       (case T of
@@ -856,7 +856,7 @@
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
-      in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
+      in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Sun Sep 05 21:41:24 2010 +0200
@@ -293,7 +293,7 @@
 in [(@{syntax_const "_Numerals"}, numeral_tr)] end
 *}
 
-typed_print_translation {*
+typed_print_translation (advanced) {*
 let
   fun dig b n = b + 2 * n; 
   fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
@@ -301,14 +301,15 @@
     | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
         dig 1 (int_of_num' n)
     | int_of_num' (Const (@{const_syntax One}, _)) = 1;
-  fun num_tr' show_sorts T [n] =
+  fun num_tr' ctxt show_sorts T [n] =
     let
       val k = int_of_num' n;
       val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
-    in case T
-     of Type (@{type_name fun}, [_, T']) =>
-         if not (! show_types) andalso can Term.dest_Type T' then t'
-         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+    in
+      case T of
+        Type (@{type_name fun}, [_, T']) =>
+          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
+          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
       | T' => if T' = dummyT then t' else raise Match
     end;
 in [(@{const_syntax of_num}, num_tr')] end
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -392,7 +392,9 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_structs_value #>
+ (register_config Syntax.show_sorts_value #>
+  register_config Syntax.show_types_value #>
+  register_config Syntax.show_structs_value #>
   register_config Syntax.show_question_marks_value #>
   register_config Syntax.ambiguity_level_value #>
   register_config Syntax.eta_contract_value #>
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -164,7 +164,7 @@
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
-      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
+      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/code.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -110,7 +110,8 @@
 
 (* printing *)
 
-fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
+fun string_of_typ thy =
+  Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
 
 fun string_of_const thy c = case AxClass.inst_of_param thy c
  of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -180,7 +180,8 @@
     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
-    fun prt_term' t = if !show_types
+    fun prt_term' t =
+      if Config.get ctxt show_types
       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
       else prt_term t;
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -215,7 +215,7 @@
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
 
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -111,10 +111,10 @@
 
 
 val display_preferences =
- [bool_pref show_types
+ [bool_pref show_types_default
     "show-types"
     "Include types in display of Isabelle terms",
-  bool_pref show_sorts
+  bool_pref show_sorts_default
     "show-sorts"
     "Include sorts in display of Isabelle terms",
   bool_pref show_consts_default
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -7,8 +7,12 @@
 signature PRINTER0 =
 sig
   val show_brackets: bool Unsynchronized.ref
-  val show_sorts: bool Unsynchronized.ref
-  val show_types: bool Unsynchronized.ref
+  val show_sorts_default: bool Unsynchronized.ref
+  val show_sorts_value: Config.value Config.T
+  val show_sorts: bool Config.T
+  val show_types_default: bool Unsynchronized.ref
+  val show_types_value: Config.value Config.T
+  val show_types: bool Config.T
   val show_free_types: bool Config.T
   val show_all_types: bool Config.T
   val show_structs_value: Config.value Config.T
@@ -49,8 +53,14 @@
 
 (** options for printing **)
 
-val show_types = Unsynchronized.ref false;
-val show_sorts = Unsynchronized.ref false;
+val show_types_default = Unsynchronized.ref false;
+val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
+val show_types = Config.bool show_types_value;
+
+val show_sorts_default = Unsynchronized.ref false;
+val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
+val show_sorts = Config.bool show_sorts_value;
+
 val show_brackets = Unsynchronized.ref false;
 val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
 val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
@@ -78,7 +88,7 @@
       | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   in app_first fns end;
 
-fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
 
 
 (* simple_ast_of *)
@@ -102,6 +112,7 @@
 
 fun ast_of_termT ctxt trf tm =
   let
+    val ctxt' = Config.put show_sorts false ctxt;
     fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
       | ast_of (Const (a, _)) = trans a []
@@ -111,19 +122,24 @@
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of ctxt t
     and trans a args =
-      ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
+      ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
+fun typ_to_ast ctxt trf T =
+  ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
 
 
 
 (** term_to_ast **)
 
-fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
+fun term_to_ast idents consts ctxt trf tm =
   let
+    val show_types =
+      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+      Config.get ctxt show_all_types;
+    val show_sorts = Config.get ctxt show_sorts;
     val show_structs = Config.get ctxt show_structs;
     val show_free_types = Config.get ctxt show_free_types;
     val show_all_types = Config.get ctxt show_all_types;
@@ -188,7 +204,7 @@
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args =
-      ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
+      ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
@@ -204,10 +220,6 @@
     |> ast_of
   end;
 
-fun term_to_ast idents consts ctxt trf tm =
-  ast_of_term idents consts ctxt trf
-    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types) (! show_sorts) tm;
-
 
 
 (** type prtabs **)
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -444,8 +444,8 @@
 
 (* options *)
 
-val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
-val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
+val _ = add_option "show_types" (Config.put show_types o boolean);
+val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
 val _ = add_option "show_structs" (Config.put show_structs o boolean);
 val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -519,7 +519,7 @@
     fun check_constraint (a, S) =
       if Sign.subsort thy (super, S) then ()
       else error ("Sort constraint of type variable " ^
-        setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
+        Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^
         " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
 
 
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/goal_display.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -77,12 +77,20 @@
 
 fun pretty_goals ctxt0 state =
   let
-    val ctxt = Config.put show_free_types false ctxt0;
+    val ctxt = ctxt0
+      |> Config.put show_free_types false
+      |> Config.put show_types
+       (Config.get ctxt0 show_types orelse
+        Config.get ctxt0 show_sorts orelse
+        Config.get ctxt0 show_all_types)
+      |> Config.put show_sorts false;
 
-    val show_all_types = Config.get ctxt show_all_types;
+    val show_sorts0 = Config.get ctxt0 show_sorts;
+    val show_types = Config.get ctxt show_types;
+    val show_consts = Config.get ctxt show_consts
+    val show_main_goal = Config.get ctxt show_main_goal;
     val goals_limit = Config.get ctxt goals_limit;
     val goals_total = Config.get ctxt goals_total;
-    val show_main_goal = Config.get ctxt show_main_goal;
 
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
@@ -120,23 +128,18 @@
     val {prop, tpairs, ...} = Thm.rep_thm state;
     val (As, B) = Logic.strip_horn prop;
     val ngoals = length As;
-
-    fun pretty_gs (types, sorts) =
-      (if show_main_goal then [prt_term B] else []) @
-       (if ngoals = 0 then [Pretty.str "No subgoals!"]
-        else if ngoals > goals_limit then
-          pretty_subgoals (take goals_limit As) @
-          (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
-           else [])
-        else pretty_subgoals As) @
-      pretty_ffpairs tpairs @
-      (if Config.get ctxt show_consts then pretty_consts prop else []) @
-      (if types then pretty_vars prop else []) @
-      (if sorts then pretty_varsT prop else []);
   in
-    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
-      (setmp_CRITICAL show_sorts false pretty_gs)
-   (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
+    (if show_main_goal then [prt_term B] else []) @
+     (if ngoals = 0 then [Pretty.str "No subgoals!"]
+      else if ngoals > goals_limit then
+        pretty_subgoals (take goals_limit As) @
+        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+         else [])
+      else pretty_subgoals As) @
+    pretty_ffpairs tpairs @
+    (if show_consts then pretty_consts prop else []) @
+    (if show_types then pretty_vars prop else []) @
+    (if show_sorts0 then pretty_varsT prop else [])
   end;
 
 fun pretty_goals_without_context th =
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/theory.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -161,11 +161,13 @@
         | TERM (msg, _) => error msg;
     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
+    val ctxt = Syntax.init_pretty_global thy
+      |> Config.put show_sorts true;
     val bad_sorts =
       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
     val _ = null bad_sorts orelse
       error ("Illegal sort constraints in primitive specification: " ^
-        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
+        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
   in
     (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   end handle ERROR msg =>
@@ -217,18 +219,18 @@
       handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT_global T;
 
-    fun message txt =
+    val ctxt = Syntax.init_pretty_global thy;
+    fun message sorts txt =
       [Pretty.block [Pretty.str "Specification of constant ",
-        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
+        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
+        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   in
     if Sign.typ_instance thy (declT, T') then ()
     else if Type.raw_instance (declT, T') then
-      error (setmp_CRITICAL show_sorts true
-        message "imposes additional sort constraints on the constant declaration")
+      error (message true "imposes additional sort constraints on the constant declaration")
     else if overloaded then ()
-    else warning (message "is strictly less general than the declared type");
-    (c, T)
+    else warning (message false "is strictly less general than the declared type")
   end;
 
 
@@ -272,7 +274,7 @@
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
     fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
-    val finalize = specify o check_overloading thy overloaded o const_of o
+    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
       Sign.cert_term thy o prep_term thy;
   in thy |> map_defs (fold finalize args) end;
 
diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Tools/nbe.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -552,10 +552,11 @@
       singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
       (Type_Infer.constrain ty' t);
-    fun check_tvars t = if null (Term.add_tvars t []) then t else
-      error ("Illegal schematic type variables in normalized term: "
-        ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
-    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
+    val string_of_term =
+      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
+    fun check_tvars t =
+      if null (Term.add_tvars t []) then t
+      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
   in
     compile_eval thy program (vs, t) deps
     |> traced (fn t => "Normalized:\n" ^ string_of_term t)