removed print_sign, print_axioms;
authorwenzelm
Wed, 11 Jan 1995 10:57:39 +0100
changeset 843 c1a4a4206102
parent 842 8d45c937a485
child 844 5e59370243fa
removed print_sign, print_axioms;
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);