src/Pure/Syntax/printer.ML

         fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
           | cons_str s syms = String s :: syms;
 
         fun arg (s, p) =
           (if s = "type" then TypArg else Arg)
-          (if is_terminal s then 1000 else p);
+          (if is_terminal s then max_pri else p);
 
         fun xsyms_to_syms (Delim s :: xsyms) =
               apfst (cons_str s) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Argument s_p :: xsyms) =
               apfst (cons (arg s_p)) (xsyms_to_syms xsyms)

     handle Symtab.DUPS cs => err_dup_fmts cs;
 
 
 
 (** pretty term or typ asts **)
+
+fun chain[Block(_,pr)] = chain(pr)
+  | chain[Arg _] = true
+  | chain _  = false;
 
 fun pretty prtab trf type_mode ast0 p0 =
   let
     val trans = apply_trans "print ast translation";
 

           let val (Ts, args') = synT (symbs, args);
           in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
       | synT (_ :: _, []) = sys_error "synT"
 
     and parT (pr, args, p, p': int) =
-      if p > p' orelse (!show_brackets andalso p' <> max_pri) then
-        #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
-      else #1 (synT (pr, args))
+          #1 (synT(if p > p' orelse
+                      (!show_brackets andalso p' <> max_pri andalso
+                       not(chain pr))
+                   then [Block (1, String "(" :: pr @ [String ")"])]
+                   else pr,
+                   args))
 
     and prefixT (_, a, [], _) = [Pretty.str a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
 
     and splitT 0 ([x], ys) = (x, ys)