src/Pure/display.ML

     fun pretty_abbrev (c, (ty, t)) = Pretty.block
       (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
 
     fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
 
+    fun pretty_finals reds = Pretty.block
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o #1) reds));
+
     fun pretty_reduct (lhs, rhs) = Pretty.block
-      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @ Pretty.commas (map prt_const' rhs));
+      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @
+        Pretty.commas (map prt_const' (sort_wrt #1 rhs)));
 
     fun pretty_restrict (const, name) =
       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val {axioms, defs, oracles} = Theory.rep_theory thy;

     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = NameSpace.extern_table constraints;
     val axms = NameSpace.extern_table axioms;
     val oras = NameSpace.extern_table oracles;
 
-    val reds = reducts |> map_filter (fn (lhs, rhs) =>
-      if null rhs then NONE
-      else SOME (apfst extern_const lhs, map (apfst extern_const) rhs)) |> sort_wrt (#1 o #1);
+    val (reds0, (reds1, reds2)) = reducts |> map (fn (lhs, rhs) =>
+        (apfst extern_const lhs, map (apfst extern_const) rhs))
+      |> sort_wrt (#1 o #1)
+      |> List.partition (null o #2)
+      ||> List.partition (Defs.plain_args o #2 o #1);
     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.names_of thy),
       Pretty.strs ("theory data:" :: Context.theory_data_of thy),
       Pretty.strs ("proof data:" :: Context.proof_data_of thy),

       Pretty.big_list "type arities:" (pretty_arities arties),
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.big_list "axioms:" (map pretty_axm axms),
+      Pretty.strs ("oracles:" :: (map #1 oras)),
       Pretty.big_list "definitions:"
-        [Pretty.big_list "open dependencies:" (map pretty_reduct reds),
-         Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)],
-      Pretty.strs ("oracles:" :: (map #1 oras))]
+        [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)]]
   end;
 
 
 
 (** print_goals **)