temporarily reverted quote change for release. breaks latex output, needs more testing. Isabelle2004_0
authorkleing
Mon, 19 Apr 2004 14:04:41 +0200
changeset 14632 805fa01ac233
parent 14631 ec1e67f88f49
child 14633 8553a957cffa
temporarily reverted quote change for release. breaks latex output, needs more testing.
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;