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 =