diff -r 1e61f23fd359 -r 0ee05eef881b src/Pure/display.ML
--- a/src/Pure/display.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/display.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -213,6 +213,11 @@
 
     fun pretty_arities (t, ars) = map (prt_arity t) ars;
 
+    fun pretty_final (c:string, tys:typ list) = Pretty.block
+      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @
+         (if null tys then [Pretty.str "<all instances>"]
+	  else Pretty.commas (map prt_typ_no_tvars tys)));
+
     fun pretty_const (c, ty) = Pretty.block
       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
 
@@ -224,6 +229,7 @@
     val spaces' = Library.sort_wrt fst spaces;
     val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
       Type.rep_tsig tsig;
+    val finals = Symtab.dest (#final_consts (rep_theory thy));
     val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
     val consts = Sign.cond_extern_table sg Sign.constK const_tab;
     val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
@@ -242,6 +248,7 @@
       Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
       Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
       Pretty.big_list "consts:" (map pretty_const consts),
+      Pretty.big_list "finals:" (map pretty_final finals),
       Pretty.big_list "axioms:" (map prt_axm axms),
       Pretty.strs ("oracles:" :: (map #1 oras))]
   end;