# HG changeset patch
# User haftmann
# Date 1356638468 -3600
# Node ID e91f6c6fb36e5924c5815e06e14ca22bcedec4ff
# Parent  e21485358c56f8c602609aa8bfb253ca47612c6d
tuned

diff -r e21485358c56 -r e91f6c6fb36e src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -261,8 +261,7 @@
   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
 
 fun brackify_infix infx fxy_ctxt (l, m, r) =
-  (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
-    ([l, str " ", m, Pretty.brk 1, r]);
+  gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
 
 fun brackify_block fxy_ctxt p1 ps p2 =
   let val p = Pretty.block_enclose (p1, p2) ps
@@ -273,11 +272,10 @@
 
 fun gen_applify strict opn cls f fxy_ctxt p [] =
       if strict
-      then (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block) [p, str "()"]
+      then gen_brackify (fixity BR fxy_ctxt) [p, str "()"]
       else p
   | gen_applify strict opn cls f fxy_ctxt p ps =
-      (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block)
-        (p @@ enum "," opn cls (map f ps));
+      gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
 
 fun applify opn = gen_applify false opn;