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