Slightly more robust proof

--- a/src/ZF/upair.ML	Fri Feb 28 15:51:06 1997 +0100
+++ b/src/ZF/upair.ML	Fri Feb 28 15:52:16 1997 +0100
@@ -76,7 +76,7 @@
 (*Classical introduction rule: no commitment to A vs B*)
 qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
  (fn prems=>
-  [ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]);
+  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
 
 AddSIs [UnCI];
 AddSEs [UnE];