src/Pure/Syntax/printer.ML

--- a/src/Pure/Syntax/printer.ML	Mon Aug 01 17:34:57 1994 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Aug 02 09:07:10 1994 +0200
@@ -7,8 +7,9 @@
 
 signature PRINTER0 =
 sig
+  val show_brackets: bool ref
+  val show_sorts: bool ref
   val show_types: bool ref
-  val show_sorts: bool ref
 end;
 
 signature PRINTER =
@@ -44,7 +45,7 @@
 
 val show_types = ref false;
 val show_sorts = ref false;
-
+val show_brackets = ref false;
 
 
 (** convert term or typ to ast **)
@@ -227,7 +228,7 @@
       | synT (_ :: _, []) = sys_error "synT"
 
     and parT (pr, args, p, p': int) =
-      if p > p' then
+      if p > p' orelse !show_brackets then
         #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
       else #1 (synT (pr, args))