# HG changeset patch
# User wenzelm
# Date 876401470 -7200
# Node ID ec27ddb5104cbca5eb0a402978b24b699733fcb8
# Parent  350150bd374431a81bfb9b679148acd95d85e651
print_theory: added oracles;

diff -r 350150bd3744 -r ec27ddb5104c src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Oct 09 14:50:39 1997 +0200
+++ b/src/Pure/display.ML	Thu Oct 09 14:51:10 1997 +0200
@@ -98,18 +98,20 @@
 
 val print_syntax = Syntax.print_syntax o syn_of;
 
-fun print_axioms thy =
+fun print_thy thy =
   let
-    val {sign, new_axioms, ...} = rep_theory thy;
+    val {sign, new_axioms, oracles, ...} = rep_theory thy;
     val axioms = Symtab.dest new_axioms;
+    val oras = map fst (Symtab.dest oracles);
 
     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
       Pretty.quote (Sign.pretty_term sign t)];
   in
-    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
+    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
+    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
   end;
 
-fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
+fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);