# HG changeset patch
# User wenzelm
# Date 1518701806 -3600
# Node ID 967213048e55e0f9c69ce33dec59e3ce1b377f0f
# Parent  560fbd6bc0474b6ed75b685ecd11b0ff556d371b
recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;

diff -r 560fbd6bc047 -r 967213048e55 src/Pure/Isar/named_target.ML
--- 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),