added print_syntax: theory -> unit;
authorwenzelm
Tue, 23 Aug 1994 19:34:01 +0200
changeset 575 74f0e5fce609
parent 574 810da101bad2
child 576 469279790410
added print_syntax: theory -> unit;
src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Aug 23 19:33:33 1994 +0200
+++ b/src/Pure/drule.ML	Tue Aug 23 19:34:01 1994 +0200
@@ -43,6 +43,7 @@
   val print_ctyp: ctyp -> unit
   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
@@ -86,7 +87,8 @@
 structure Thm = Thm;
 structure Sign = Thm.Sign;
 structure Type = Sign.Type;
-structure Pretty = Sign.Syntax.Pretty
+structure Syntax = Sign.Syntax;
+structure Pretty = Syntax.Pretty
 structure Symtab = Sign.Symtab;
 
 local open Thm
@@ -300,6 +302,8 @@
 
 val pprint_theory = Sign.pprint_sg o sign_of;
 
+val print_syntax = Syntax.print_syntax o syn_of;
+
 val print_sign = Sign.print_sg o sign_of;
 
 fun print_axioms thy =