diff -r e3d25e751d05 -r e21485358c56 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
@@ -67,6 +67,7 @@
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+  val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
@@ -270,11 +271,16 @@
     else p
   end;
 
-fun applify opn cls f fxy_ctxt p [] = p
-  | applify opn cls f fxy_ctxt p ps =
+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 "()"]
+      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));
 
+fun applify opn = gen_applify false opn;
+
 fun tuplify _ _ [] = NONE
   | tuplify print fxy [x] = SOME (print fxy x)
   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));