src/Pure/drule.ML
changeset 843 c1a4a4206102
parent 776 df8f91c0e57c
child 922 196ca0973a6d
     1.1 --- a/src/Pure/drule.ML	Wed Jan 11 10:53:22 1995 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Jan 11 10:57:39 1995 +0100
     1.3 @@ -47,8 +47,6 @@
     1.4    val print_goals	: int -> thm -> unit
     1.5    val print_goals_ref	: (int -> thm -> unit) ref
     1.6    val print_syntax	: theory -> unit
     1.7 -  val print_sign	: theory -> unit
     1.8 -  val print_axioms	: theory -> unit
     1.9    val print_theory	: theory -> unit
    1.10    val print_thm		: thm -> unit
    1.11    val prth		: thm -> thm
    1.12 @@ -336,8 +334,6 @@
    1.13  
    1.14  val print_syntax = Syntax.print_syntax o syn_of;
    1.15  
    1.16 -val print_sign = Sign.print_sg o sign_of;
    1.17 -
    1.18  fun print_axioms thy =
    1.19    let
    1.20      val {sign, new_axioms, ...} = rep_theory thy;
    1.21 @@ -349,7 +345,7 @@
    1.22      Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
    1.23    end;
    1.24  
    1.25 -fun print_theory thy = (print_sign thy; print_axioms thy);
    1.26 +fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
    1.27  
    1.28  
    1.29