--- 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 =