--- 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