# HG changeset patch
# User wenzelm
# Date 1442993778 -7200
# Node ID 2be9ea29f9eccae14fc31e6468bd8bf732c515fc
# Parent  d4af13517fd63eeae6bee070ed3b91cbb83030e0
tuned output;

diff -r d4af13517fd6 -r 2be9ea29f9ec src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Sep 23 09:30:12 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Sep 23 09:36:18 2015 +0200
@@ -123,9 +123,10 @@
     val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1);
   in
     Pretty.big_list "definitions:"
-      [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
-       Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
-       Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)]
+      (map (Pretty.text_fold o single)
+        [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
+         Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
+         Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
   end;