src/Pure/Syntax/printer.ML

 Pretty printing of asts, terms, types and print (ast) translation.
 *)
 
 signature BASIC_PRINTER =
 sig
-  val show_brackets: bool Config.T
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_markup: bool Config.T
   val show_consts_markup: bool Config.T
   val show_structs: bool Config.T

 structure Printer: PRINTER =
 struct
 
 (** options for printing **)
 
-val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
 val show_types = Config.declare_option_bool ("show_types", \<^here>);
 val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
 val show_markup_default = Unsynchronized.ref false;
 val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
 val show_consts_markup = Config.declare_bool ("show_consts_markup", \<^here>) (K true);

   markup_syntax: string -> Markup.T list,
   pretty_entity: string -> Pretty.T};
 
 fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) =
   let
-    val show_brackets = Config.get ctxt show_brackets;
-
     val application =
       if type_mode then Syntax_Trans.tappl_ast_tr'
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 

         SOME prt => SOME [prt]
       | NONE => Option.map (main p) (SOME (#trf ops a ctxt args) handle Match => NONE))
 
     and parens p q a (symbs, args) constraint =
       let
-        val symbs' =
-          if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
-          then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
+        val symbs' = if p > q then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
         val output =
           (case constraint of
             SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) =>
               Pretty.make_block (#constrain_block ops ty) o single
           | _ => I);