obsolete, cf. Proof_Context.print_syntax;
authorwenzelm
Sat, 30 Mar 2013 11:43:17 +0100
changeset 51582 a6b1f63ae1cb
parent 51581 587c917e8d36
child 51583 9100c8e66b69
obsolete, cf. Proof_Context.print_syntax;
src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Mar 29 22:26:25 2013 +0100
+++ b/src/Pure/display.ML	Sat Mar 30 11:43:17 2013 +0100
@@ -26,7 +26,6 @@
   val string_of_thm_global: theory -> thm -> string
   val string_of_thm_without_context: thm -> string
   val pretty_thms: Proof.context -> thm list -> Pretty.T
-  val print_syntax: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T list
 end;
 
@@ -101,9 +100,6 @@
 
 (** print theory **)
 
-val print_syntax = Syntax.print_syntax o Sign.syn_of;
-
-
 (* pretty_full_theory *)
 
 fun pretty_full_theory verbose thy =