# HG changeset patch
# User wenzelm
# Date 1125583090 -7200
# Node ID 64242b791c19a625545b2b9c6cf0bcddea36d796
# Parent  954c0f26520322acdf48bb46d66a34845a979956
removed obsolete 'symbols' mode;

diff -r 954c0f265203 -r 64242b791c19 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Sep 01 15:58:08 2005 +0200
+++ b/src/Pure/General/symbol.ML	Thu Sep 01 15:58:10 2005 +0200
@@ -56,7 +56,6 @@
   val default_output: string -> string * real
   val default_indent: string * int -> string
   val default_raw: string -> string
-  val symbolsN: string
   val xsymbolsN: string
   val symbol_output: string -> string * real
 end;
@@ -488,7 +487,6 @@
 
 (* xsymbols *)
 
-val symbolsN = "symbols";    (*legacy!*)
 val xsymbolsN = "xsymbols";
 
 fun sym_len s =
diff -r 954c0f265203 -r 64242b791c19 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:08 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:10 2005 +0200
@@ -154,7 +154,7 @@
 (* print mode *)
 
 val latexN = "latex";
-val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
+val modes = [latexN, Symbol.xsymbolsN];
 
 fun latex_output str =
   let val syms = Symbol.explode str