1.1 --- a/src/Pure/display.ML	Fri Jun 05 14:22:11 1998 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Jun 05 14:23:07 1998 +0200
     1.3 @@ -27,7 +27,6 @@
     1.4    val pretty_theory	: theory -> Pretty.T
     1.5    val pprint_theory	: theory -> pprint_args -> unit
     1.6    val print_syntax	: theory -> unit
     1.7 -  val print_data	: theory -> string -> unit
     1.8    val print_theory	: theory -> unit
     1.9    val pretty_name_space : string * NameSpace.T -> Pretty.T
    1.10    val show_consts	: bool ref
    1.11 @@ -106,7 +105,6 @@
    1.12  val pprint_theory = Sign.pprint_sg o sign_of;
    1.13  
    1.14  val print_syntax = Syntax.print_syntax o syn_of;
    1.15 -val print_data = Sign.print_data o sign_of;
    1.16  
    1.17  
    1.18  (* pretty_name_space  *)
    1.19 @@ -192,8 +190,7 @@
    1.20          Pretty.quote (Sign.pretty_term sign t)];
    1.21    in
    1.22      Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms));
    1.23 -    Pretty.writeln (Pretty.strs ("oracles:" :: oras));
    1.24 -    print_data thy "Pure/theorems"	(*forward reference!*)
    1.25 +    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
    1.26    end;
    1.27  
    1.28  fun print_theory thy = (print_sign (sign_of thy); print_thy thy);