# HG changeset patch
# User kleing
# Date 1082376281 -7200
# Node ID 805fa01ac2337790fd555991f1231d3ef6b2e3fb
# Parent  ec1e67f88f4970cf9adeec457eeccffbe35ac0c4
temporarily reverted quote change for release. breaks latex output, needs more testing.

diff -r ec1e67f88f49 -r 805fa01ac233 src/Pure/General/symbol.ML
--- 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;