1.1 --- a/src/Pure/Syntax/printer.ML	Fri May 24 19:09:56 2013 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Mon May 27 18:24:38 2013 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4    val show_types: bool Config.T
     1.5    val show_sorts: bool Config.T
     1.6    val show_free_types: bool Config.T
     1.7 -  val show_all_types: bool Config.T
     1.8    val show_markup: bool Config.T
     1.9    val show_structs: bool Config.T
    1.10    val show_question_marks: bool Config.T
    1.11 @@ -60,7 +59,6 @@
    1.12  val show_sorts = Config.bool show_sorts_raw;
    1.13  
    1.14  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    1.15 -val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
    1.16  
    1.17  val show_markup_default = Unsynchronized.ref false;
    1.18  val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));

     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri May 24 19:09:56 2013 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 18:24:38 2013 +0200
     2.3 @@ -545,12 +545,9 @@
     2.4  
     2.5  fun term_to_ast idents is_syntax_const ctxt trf tm =
     2.6    let
     2.7 -    val show_types =
     2.8 -      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
     2.9 -      Config.get ctxt show_all_types;
    2.10 +    val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
    2.11      val show_structs = Config.get ctxt show_structs;
    2.12      val show_free_types = Config.get ctxt show_free_types;
    2.13 -    val show_all_types = Config.get ctxt show_all_types;
    2.14      val show_markup = Config.get ctxt show_markup;
    2.15  
    2.16      val {structs, fixes} = idents;
    2.17 @@ -610,10 +607,7 @@
    2.18            in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
    2.19        | (Const ("_idtdummy", T), ts) =>
    2.20            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    2.21 -      | (const as Const (c, T), ts) =>
    2.22 -          if show_all_types
    2.23 -          then Ast.mk_appl (constrain const T) (map ast_of ts)
    2.24 -          else trans c T ts
    2.25 +      | (const as Const (c, T), ts) => trans c T ts
    2.26        | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
    2.27  
    2.28      and trans a T args = ast_of (trf a ctxt T args)
    2.29 @@ -666,9 +660,7 @@
    2.30    let
    2.31      val show_markup = Config.get ctxt show_markup;
    2.32      val show_sorts = Config.get ctxt show_sorts;
    2.33 -    val show_types =
    2.34 -      Config.get ctxt show_types orelse show_sorts orelse
    2.35 -      Config.get ctxt show_all_types;
    2.36 +    val show_types = Config.get ctxt show_types orelse show_sorts;
    2.37  
    2.38      val syn = Proof_Context.syn_of ctxt;
    2.39      val prtabs = Syntax.prtabs syn;

     3.1 --- a/src/Pure/goal_display.ML	Fri May 24 19:09:56 2013 +0200
     3.2 +++ b/src/Pure/goal_display.ML	Mon May 27 18:24:38 2013 +0200
     3.3 @@ -71,10 +71,7 @@
     3.4    let
     3.5      val ctxt = ctxt0
     3.6        |> Config.put show_free_types false
     3.7 -      |> Config.put show_types
     3.8 -       (Config.get ctxt0 show_types orelse
     3.9 -        Config.get ctxt0 show_sorts orelse
    3.10 -        Config.get ctxt0 show_all_types)
    3.11 +      |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
    3.12        |> Config.put show_sorts false;
    3.13  
    3.14      val show_sorts0 = Config.get ctxt0 show_sorts;