# HG changeset patch
# User wenzelm
# Date 1442993412 -7200
# Node ID d4af13517fd63eeae6bee070ed3b91cbb83030e0
# Parent  9ce5de06cd3b0a6f07d1e183e9d8c768138da352
tuned output;

diff -r 9ce5de06cd3b -r d4af13517fd6 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 22 22:42:48 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Sep 23 09:30:12 2015 +0200
@@ -102,9 +102,6 @@
 
     fun sort_items f = sort (Defs.item_ord o apply2 (snd o f));
 
-    fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_entry o fst) reds));
-
     fun pretty_reduct (lhs, rhs) = Pretty.block
       ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
         Pretty.commas (map pretty_entry (sort_items fst rhs)));
@@ -115,21 +112,20 @@
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
 
-    val (reds0, (reds1, reds2)) =
+    val (reds1, reds2) =
       filter_out (prune_item o #1 o #1) reducts
       |> map (fn (lhs, rhs) =>
         (apfst markup_extern_item lhs, map (apfst markup_extern_item) (filter_out (prune_item o fst) rhs)))
       |> sort_items (#1 o #1)
-      |> List.partition (null o #2)
-      ||> List.partition (Defs.plain_args o #2 o #1);
+      |> filter_out (null o #2)
+      |> List.partition (Defs.plain_args o #2 o #1);
 
     val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1);
   in
     Pretty.big_list "definitions:"
-      [pretty_finals reds0,
-       Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
-       Pretty.big_list "overloaded:" (map pretty_reduct reds2),
-       Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]
+      [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;