# HG changeset patch
# User wenzelm
# Date 777663241 -7200
# Node ID 74f0e5fce609fb66ce6f8fdf6d213dbf46400e99
# Parent  810da101bad27d272972b588005e42cf87dc0271
added print_syntax: theory -> unit;

diff -r 810da101bad2 -r 74f0e5fce609 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 =