src/Pure/General/symbol.ML
changeset 14632 805fa01ac233
parent 14609 663e0e435866
child 14678 662b181cae05
--- 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;