# HG changeset patch
# User wenzelm
# Date 1127948337 -7200
# Node ID f776b3bf4126b1e9c00b51f754cc3137eeb73f2d
# Parent  6ec36bad47ea249ad64b85e7359309397a69a366
print_theory: discontinued final consts;

diff -r 6ec36bad47ea -r f776b3bf4126 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Sep 29 00:58:56 2005 +0200
+++ b/src/Pure/display.ML	Thu Sep 29 00:58:57 2005 +0200
@@ -192,14 +192,9 @@
     fun pretty_const (c, ty) = Pretty.block
       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
 
-    fun pretty_final (c, []) = Pretty.str c
-      | pretty_final (c, tys) = Pretty.block
-          (Pretty.str c :: Pretty.str " ::" :: Pretty.brk 1 ::
-             Pretty.commas (map prt_typ_no_tvars tys));
-
     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
 
-    val {axioms, defs, oracles} = Theory.rep_theory thy;
+    val {axioms, defs = _, oracles} = Theory.rep_theory thy;
     val {naming, syn = _, tsig, consts = (consts, constraints)} = Sign.rep_sg thy;
     val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
 
@@ -208,7 +203,6 @@
     val arties = NameSpace.dest_table (Sign.type_space thy, arities);
     val cnsts = NameSpace.extern_table consts |> map (apsnd fst);
     val cnsts' = NameSpace.extern_table (#1 consts, constraints);
-    val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
     val axms = NameSpace.extern_table axioms;
     val oras = NameSpace.extern_table oracles;
   in
@@ -224,7 +218,6 @@
       Pretty.big_list "type arities:" (pretty_arities arties),
       Pretty.big_list "consts:" (map pretty_const cnsts),
       Pretty.big_list "const constraints:" (map pretty_const cnsts'),
-      Pretty.big_list "finals consts:" (map pretty_final finals),
       Pretty.big_list "axioms:" (map prt_axm axms),
       Pretty.strs ("oracles:" :: (map #1 oras))]
   end;