# HG changeset patch
# User wenzelm
# Date 1129751567 -7200
# Node ID ab08250b80dfbd076dfb3b145ec818f07cd1b4e9
# Parent  b8f2dd8858f64ada6d51bd67873cc6ff1365d90d
removed obsolete old_symbol_source;

diff -r b8f2dd8858f6 -r ab08250b80df src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Oct 19 21:52:46 2005 +0200
+++ b/src/Pure/Thy/present.ML	Wed Oct 19 21:52:47 2005 +0200
@@ -22,7 +22,6 @@
   val finish: unit -> unit
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
-  val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
   val begin_theory: Path.T option -> string -> string list ->
     (Path.T * bool) list -> theory -> theory
@@ -431,10 +430,6 @@
 fun verbatim_source name mk_text =
   with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
 
-fun old_symbol_source name mk_text =
-  with_session () (fn _ => add_tex_source name
-    (Latex.symbol_source (K true, K true) name (mk_text ())));
-
 fun theory_output name s =
   with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));