Fix a duplicate abbreviation || in etc/symbols.

--- a/etc/symbols	Thu Oct 22 17:54:47 2009 +0200
+++ b/etc/symbols	Fri Oct 23 09:20:22 2009 +1100
@@ -244,7 +244,7 @@
 \<Inter>                code: 0x0022c2  font: Isabelle  abbrev: Inter
 \<union>                code: 0x00222a  font: Isabelle  abbrev: Un
 \<Union>                code: 0x0022c3  font: Isabelle  abbrev: Union
-\<squnion>              code: 0x002294  font: Isabelle  abbrev: ||
+\<squnion>              code: 0x002294  font: Isabelle  abbrev: |_|
 \<Squnion>              code: 0x002a06  font: Isabelle  abbrev: |||
 \<sqinter>              code: 0x002293  font: Isabelle  abbrev: &&
 \<Sqinter>              code: 0x002a05  font: Isabelle  abbrev: &&&