# HG changeset patch
# User wenzelm
# Date 1369671878 -7200
# Node ID 1b481b4904549d6c86c852ae7c62fadf81490c21
# Parent  667961fa6a605a5627c2e4261adb7c0166ab55f3
discontinued obsolete show_all_types;

diff -r 667961fa6a60 -r 1b481b490454 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri May 24 19:09:56 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon May 27 18:24:38 2013 +0200
@@ -10,7 +10,6 @@
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_free_types: bool Config.T
-  val show_all_types: bool Config.T
   val show_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
@@ -60,7 +59,6 @@
 val show_sorts = Config.bool show_sorts_raw;
 
 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));
 
 val show_markup_default = Unsynchronized.ref false;
 val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
diff -r 667961fa6a60 -r 1b481b490454 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri May 24 19:09:56 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 18:24:38 2013 +0200
@@ -545,12 +545,9 @@
 
 fun term_to_ast idents is_syntax_const 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_types = Config.get ctxt show_types orelse 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;
     val show_markup = Config.get ctxt show_markup;
 
     val {structs, fixes} = idents;
@@ -610,10 +607,7 @@
           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
-      | (const as Const (c, T), ts) =>
-          if show_all_types
-          then Ast.mk_appl (constrain const T) (map ast_of ts)
-          else trans c T ts
+      | (const as Const (c, T), ts) => trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args = ast_of (trf a ctxt T args)
@@ -666,9 +660,7 @@
   let
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
-    val show_types =
-      Config.get ctxt show_types orelse show_sorts orelse
-      Config.get ctxt show_all_types;
+    val show_types = Config.get ctxt show_types orelse show_sorts;
 
     val syn = Proof_Context.syn_of ctxt;
     val prtabs = Syntax.prtabs syn;
diff -r 667961fa6a60 -r 1b481b490454 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri May 24 19:09:56 2013 +0200
+++ b/src/Pure/goal_display.ML	Mon May 27 18:24:38 2013 +0200
@@ -71,10 +71,7 @@
   let
     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_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
       |> Config.put show_sorts false;
 
     val show_sorts0 = Config.get ctxt0 show_sorts;