improved print_data;
authorwenzelm
Wed Oct 15 15:13:25 1997 +0200 (1997-10-15)
changeset 387364f496e0885d
parent 3872 a5839ecee7b8
child 3874 552ce5ad6a2e
improved print_data;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Wed Oct 15 15:12:59 1997 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Oct 15 15:13:25 1997 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val print_goals	: int -> thm -> unit
     1.5    val print_syntax	: theory -> unit
     1.6    val print_theory	: theory -> unit
     1.7 +  val print_data	: theory -> string -> unit
     1.8    val print_thm		: thm -> unit
     1.9    val prth		: thm -> thm
    1.10    val prthq		: thm Sequence.seq -> thm Sequence.seq
    1.11 @@ -98,6 +99,7 @@
    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  fun print_thy thy =
    1.18    let
    1.19 @@ -109,8 +111,7 @@
    1.20        Pretty.quote (Sign.pretty_term sign t)];
    1.21    in
    1.22      Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
    1.23 -    Pretty.writeln (Pretty.strs ("oracles:" :: oras));
    1.24 -    Sign.print_data sign
    1.25 +    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
    1.26    end;
    1.27  
    1.28  fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);