# HG changeset patch
# User wenzelm
# Date 1364640197 -3600
# Node ID a6b1f63ae1cb19c6fd1eaab4cc04e422f8bb7322
# Parent  587c917e8d36f3ba47b0b7def9540e6d6c4619c4
obsolete, cf. Proof_Context.print_syntax;

diff -r 587c917e8d36 -r a6b1f63ae1cb 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 =