# HG changeset patch
# User paulson
# Date 857141536 -3600
# Node ID dabe8ab631fadf9e90296fcd43f61ae9daf8ec60
# Parent  6d3d893453de42eda81f04d884701c00450315f9
Slightly more robust proof

diff -r 6d3d893453de -r dabe8ab631fa src/ZF/upair.ML
--- 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];