Changes

Summary

recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;

Changeset 67615:967213048e55 by wenzelm: recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
The file was modified	`src/Pure/Isar/named_target.ML` (diff)