src/Pure/display.ML
changeset 17704 f776b3bf4126
parent 17475 d008d04068a1
child 17995 8b9c6af78a67
     1.1 --- a/src/Pure/display.ML	Thu Sep 29 00:58:56 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Sep 29 00:58:57 2005 +0200
     1.3 @@ -192,14 +192,9 @@
     1.4      fun pretty_const (c, ty) = Pretty.block
     1.5        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
     1.6  
     1.7 -    fun pretty_final (c, []) = Pretty.str c
     1.8 -      | pretty_final (c, tys) = Pretty.block
     1.9 -          (Pretty.str c :: Pretty.str " ::" :: Pretty.brk 1 ::
    1.10 -             Pretty.commas (map prt_typ_no_tvars tys));
    1.11 -
    1.12      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.13  
    1.14 -    val {axioms, defs, oracles} = Theory.rep_theory thy;
    1.15 +    val {axioms, defs = _, oracles} = Theory.rep_theory thy;
    1.16      val {naming, syn = _, tsig, consts = (consts, constraints)} = Sign.rep_sg thy;
    1.17      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.18  
    1.19 @@ -208,7 +203,6 @@
    1.20      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.21      val cnsts = NameSpace.extern_table consts |> map (apsnd fst);
    1.22      val cnsts' = NameSpace.extern_table (#1 consts, constraints);
    1.23 -    val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
    1.24      val axms = NameSpace.extern_table axioms;
    1.25      val oras = NameSpace.extern_table oracles;
    1.26    in
    1.27 @@ -224,7 +218,6 @@
    1.28        Pretty.big_list "type arities:" (pretty_arities arties),
    1.29        Pretty.big_list "consts:" (map pretty_const cnsts),
    1.30        Pretty.big_list "const constraints:" (map pretty_const cnsts'),
    1.31 -      Pretty.big_list "finals consts:" (map pretty_final finals),
    1.32        Pretty.big_list "axioms:" (map prt_axm axms),
    1.33        Pretty.strs ("oracles:" :: (map #1 oras))]
    1.34    end;