temporarily reverted quote change for release. breaks latex output, needs more testing. Isabelle2004_0
authorkleing
Mon Apr 19 14:04:41 2004 +0200 (2004-04-19)
changeset 14632805fa01ac233
parent 14631 ec1e67f88f49
child 14633 8553a957cffa
temporarily reverted quote change for release. breaks latex output, needs more testing.
src/Pure/General/symbol.ML
     1.1 --- a/src/Pure/General/symbol.ML	Mon Apr 19 13:49:35 2004 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Mon Apr 19 14:04:41 2004 +0200
     1.3 @@ -321,9 +321,3 @@
     1.4  val escape = sym_escape;
     1.5  
     1.6  end;
     1.7 -
     1.8 -
     1.9 -(* Overwrites versions in Library *)
    1.10 -
    1.11 -val quote = Symbol.quote;
    1.12 -val commas_quote = Symbol.commas_quote;