diff -r ef4c41e7956a -r e94aa103e12d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 20 11:10:24 2003 +0100
+++ b/src/HOL/Set.thy	Tue Feb 25 12:42:08 2003 +0100
@@ -157,8 +157,7 @@
     let val (x,t) = atomic_abs_tr' abs
     in Syntax.const syn $ x $ A $ t end
 in
-[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
- ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
+[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
 end
 *}