# HG changeset patch
# User wenzelm
# Date 876921205 -7200
# Node ID 64f496e0885daa0fbbe15b4d80c865f5e8b25b5f
# Parent  a5839ecee7b84e610543c6a7b4fd778f8977e1ef
improved print_data;

diff -r a5839ecee7b8 -r 64f496e0885d src/Pure/display.ML
--- a/src/Pure/display.ML	Wed Oct 15 15:12:59 1997 +0200
+++ b/src/Pure/display.ML	Wed Oct 15 15:13:25 1997 +0200
@@ -20,6 +20,7 @@
   val print_goals	: int -> thm -> unit
   val print_syntax	: theory -> unit
   val print_theory	: theory -> unit
+  val print_data	: theory -> string -> unit
   val print_thm		: thm -> unit
   val prth		: thm -> thm
   val prthq		: thm Sequence.seq -> thm Sequence.seq
@@ -98,6 +99,7 @@
 val pprint_theory = Sign.pprint_sg o sign_of;
 
 val print_syntax = Syntax.print_syntax o syn_of;
+val print_data = Sign.print_data o sign_of;
 
 fun print_thy thy =
   let
@@ -109,8 +111,7 @@
       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));
-    Sign.print_data sign
+    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
   end;
 
 fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);