src/Tools/Code/code_printer.ML

   val INFX: int * lrx -> fixity
   val APP: fixity
   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 applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
+  val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
 
   type tyco_syntax
   type simple_const_syntax
   type proto_const_syntax
   type const_syntax

   in if fixity BR fxy_ctxt
     then enclose "(" ")" [p]
     else p
   end;
 
-fun applify opn cls fxy_ctxt p [] = p
-  | applify opn cls fxy_ctxt p ps =
+fun applify opn cls f fxy_ctxt p [] = p
+  | applify opn cls f fxy_ctxt p ps =
       (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
-        (p @@ enum "," opn cls ps);
+        (p @@ enum "," opn cls (map f ps));
 
 
 (* generic syntax *)
 
 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)