diff -r 32c5251f78cd -r 97097e589715 src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Tue Jun 01 13:52:11 2010 +0200
@@ -31,11 +31,11 @@
   end;
 
 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
-  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
+  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
     pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
     Code_Printer.str target_cons,
     pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
-  ];
+  );
 
 fun add_literal_list target =
   let