diff -r 2116425cebc8 -r 82f9ce5a8274 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Jun 29 17:03:59 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Wed Jun 30 11:38:51 2010 +0200
@@ -63,7 +63,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 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
@@ -230,10 +230,10 @@
     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 *)