Sign.print_data;

--- a/src/Pure/display.ML	Tue Oct 14 17:35:35 1997 +0200
+++ b/src/Pure/display.ML	Tue Oct 14 17:35:56 1997 +0200
@@ -109,7 +109,8 @@
       Pretty.quote (Sign.pretty_term sign t)];
   in
     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
-    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
+    Pretty.writeln (Pretty.strs ("oracles:" :: oras));
+    Sign.print_data sign
   end;
 
 fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);