--- a/src/HOL/Set.ML Thu Sep 27 16:04:11 2001 +0200
+++ b/src/HOL/Set.ML Thu Sep 27 16:04:25 2001 +0200
@@ -422,7 +422,7 @@
by (Asm_simp_tac 1);
qed "UnI2";
-AddXIs [UnI1, UnI2];
+AddXEs [UnI1, UnI2];
(*Classical introduction rule: no commitment to A vs B*)