removed obsolete old_symbol_source;
authorwenzelm
Wed, 19 Oct 2005 21:52:47 +0200
changeset 17934 ab08250b80df
parent 17933 b8f2dd8858f6
child 17935 c6f1442ce949
removed obsolete old_symbol_source;
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));