# HG changeset patch
# User wenzelm
# Date 789818259 -3600
# Node ID c1a4a42061025c41b6854e9479cde5e3e26fce84
# Parent  8d45c937a485852bac83224be036e38b38a2315e
removed print_sign, print_axioms;

diff -r 8d45c937a485 -r c1a4a4206102 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jan 11 10:53:22 1995 +0100
+++ b/src/Pure/drule.ML	Wed Jan 11 10:57:39 1995 +0100
@@ -47,8 +47,6 @@
   val print_goals	: int -> thm -> unit
   val print_goals_ref	: (int -> thm -> unit) ref
   val print_syntax	: theory -> unit
-  val print_sign	: theory -> unit
-  val print_axioms	: theory -> unit
   val print_theory	: theory -> unit
   val print_thm		: thm -> unit
   val prth		: thm -> thm
@@ -336,8 +334,6 @@
 
 val print_syntax = Syntax.print_syntax o syn_of;
 
-val print_sign = Sign.print_sg o sign_of;
-
 fun print_axioms thy =
   let
     val {sign, new_axioms, ...} = rep_theory thy;
@@ -349,7 +345,7 @@
     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
   end;
 
-fun print_theory thy = (print_sign thy; print_axioms thy);
+fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);