temporarily reverted quote change for release. breaks latex output, needs more testing.
--- a/src/Pure/General/symbol.ML Mon Apr 19 13:49:35 2004 +0200
+++ b/src/Pure/General/symbol.ML Mon Apr 19 14:04:41 2004 +0200
@@ -321,9 +321,3 @@
val escape = sym_escape;
end;
-
-
-(* Overwrites versions in Library *)
-
-val quote = Symbol.quote;
-val commas_quote = Symbol.commas_quote;