recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
--- a/src/Pure/Isar/named_target.ML Thu Feb 15 13:04:36 2018 +0100
+++ b/src/Pure/Isar/named_target.ML Thu Feb 15 14:36:46 2018 +0100
@@ -104,7 +104,8 @@
declaration = Generic_Target.locale_declaration locale,
theory_registration = fn _ => error "Not possible in locale target",
locale_dependency = Generic_Target.locale_dependency locale,
- pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale}
+ pretty = fn ctxt =>
+ [Pretty.block (Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale)]}
| operations (Class class) =
{define = Generic_Target.define (class_foundation class),
notes = Generic_Target.notes (Generic_Target.locale_target_notes class),