# HG changeset patch
# User wenzelm
# Date 927296559 -7200
# Node ID 05c56f41e661672740f8d72a656a2b532f2ec2f3
# Parent  8a1b5f9d842096abe4c6b9fed84d521f9ef00440
avoid string constants;

diff -r 8a1b5f9d8420 -r 05c56f41e661 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri May 21 12:11:13 1999 +0200
+++ b/src/Pure/General/symbol.ML	Fri May 21 16:22:39 1999 +0200
@@ -29,6 +29,9 @@
   val explode: string -> symbol list
   val input: string -> string
   val add_mode: string -> (string -> string * real) -> unit
+  val isabelle_fontN: string
+  val symbolsN: string
+  val xsymbolsN: string
   val output: string -> string
   val output_width: string -> string * real
 end;
@@ -309,7 +312,11 @@
 
 (* maintain modes *)
 
-val modes = ref (Symtab.make [("isabelle_font", isabelle_font_output)]);
+val isabelle_fontN = "isabelle_font";
+val symbolsN = "symbols";
+val xsymbolsN = "xsymbols";
+
+val modes = ref (Symtab.make [(isabelle_fontN, isabelle_font_output)]);
 
 fun lookup_mode name = Symtab.lookup (! modes, name);
 
diff -r 8a1b5f9d8420 -r 05c56f41e661 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri May 21 12:11:13 1999 +0200
+++ b/src/Pure/pure_thy.ML	Fri May 21 16:22:39 1999 +0200
@@ -417,8 +417,8 @@
     ("itself", [logicS], logicS)]
   |> Theory.add_nonterminals Syntax.pure_nonterms
   |> Theory.add_syntax Syntax.pure_syntax
-  |> Theory.add_modesyntax ("symbols" , true) Syntax.pure_sym_syntax
-  |> Theory.add_modesyntax ("xsymbols", true) Syntax.pure_xsym_syntax
+  |> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax
+  |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Theory.add_syntax