# HG changeset patch
# User nipkow
# Date 1046173328 -3600
# Node ID e94aa103e12d5214fced6fa54738e189652ab560
# Parent  ef4c41e7956affc33f9b96a4f64625fc690e5e47
Undid eta change for UN/INT.

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
 *}