removed obsolete 'symbols' mode;
authorwenzelm
Thu Sep 01 15:58:10 2005 +0200 (2005-09-01)
changeset 1721864242b791c19
parent 17217 954c0f265203
child 17219 515badbfc4d6
removed obsolete 'symbols' mode;
src/Pure/General/symbol.ML
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/General/symbol.ML	Thu Sep 01 15:58:08 2005 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Thu Sep 01 15:58:10 2005 +0200
     1.3 @@ -56,7 +56,6 @@
     1.4    val default_output: string -> string * real
     1.5    val default_indent: string * int -> string
     1.6    val default_raw: string -> string
     1.7 -  val symbolsN: string
     1.8    val xsymbolsN: string
     1.9    val symbol_output: string -> string * real
    1.10  end;
    1.11 @@ -488,7 +487,6 @@
    1.12  
    1.13  (* xsymbols *)
    1.14  
    1.15 -val symbolsN = "symbols";    (*legacy!*)
    1.16  val xsymbolsN = "xsymbols";
    1.17  
    1.18  fun sym_len s =
     2.1 --- a/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:08 2005 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:10 2005 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4  (* print mode *)
     2.5  
     2.6  val latexN = "latex";
     2.7 -val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
     2.8 +val modes = [latexN, Symbol.xsymbolsN];
     2.9  
    2.10  fun latex_output str =
    2.11    let val syms = Symbol.explode str