# HG changeset patch
# User paulson
# Date 856535924 -3600
# Node ID 1b266c1611344e8c24933e5142e4a8a709f73fa5
# Parent  85d7e800d7548f959922564ac29f6f28c2ffdd24
More robust proof (?)

diff -r 85d7e800d754 -r 1b266c161134 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Fri Feb 21 15:31:47 1997 +0100
+++ b/src/ZF/upair.ML	Fri Feb 21 15:38:44 1997 +0100
@@ -167,7 +167,7 @@
 (*Classical introduction rule*)
 qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  (fn prems=>
-  [ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]);
+  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
 
 AddSIs [consCI];
 AddSEs [consE];