changeset 82380 | ceb4f33d3073 |
parent 82248 | e8c96013ea8a |
child 82599 | 98571d7e4a7d |
--- a/src/HOL/List.thy Sun Mar 30 13:50:06 2025 +0200 +++ b/src/HOL/List.thy Sun Mar 30 13:50:06 2025 +0200 @@ -8156,7 +8156,7 @@ fun print_list (target_fxy, target_cons) pr fxy t1 t2 = 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, + Pretty.str target_cons, pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2 );