src/Pure/display.ML

 
     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.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);