diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/OrdQuant.thy	Wed Dec 19 11:13:27 2001 +0100
@@ -26,9 +26,9 @@
   "UN x<a. B"   == "OUnion(a, %x. B)"
 
 syntax (xsymbols)
-  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
-  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
-  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
+  "@oall"     :: [idt, i, o] => o        ("(3\\<forall>_<_./ _)" 10)
+  "@oex"      :: [idt, i, o] => o        ("(3\\<exists>_<_./ _)" 10)
+  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union>_<_./ _)" 10)
 
 defs