--- 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;