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