Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned output;
authorwenzelm
Wed, 23 Sep 2015 09:36:18 +0200
changeset 61258 2be9ea29f9ec
parent 61257 d4af13517fd6
child 61259 6dc3d5d50e57
tuned output;
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle