src/HOL/List.thy
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
   );