src/Pure/display.ML
changeset 28290 4cc2b6046258
parent 28288 09c812966e7f
child 28316 b17d863a050f
     1.1 --- a/src/Pure/display.ML	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -178,7 +178,6 @@
     1.4        Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
     1.5  
     1.6      val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     1.7 -    val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
     1.8      val defs = Theory.defs_of thy;
     1.9      val {restricts, reducts} = Defs.dest defs;
    1.10      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    1.11 @@ -202,7 +201,6 @@
    1.12      val cnstrs = NameSpace.extern_table constraints;
    1.13  
    1.14      val axms = NameSpace.extern_table axioms;
    1.15 -    val oras = NameSpace.extern_table oracles;
    1.16  
    1.17      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
    1.18        |> map (fn (lhs, rhs) =>
    1.19 @@ -223,7 +221,7 @@
    1.20        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    1.21        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
    1.22        Pretty.big_list "axioms:" (map pretty_axm axms),
    1.23 -      Pretty.strs ("oracles:" :: (map #1 oras)),
    1.24 +      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
    1.25        Pretty.big_list "definitions:"
    1.26          [pretty_finals reds0,
    1.27           Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),