# HG changeset patch
# User lcp
# Date 785669507 -3600
# Node ID 3054a10ed5b5052a35b7deb218d026b10c5f8055
# Parent  436019ca97d7b22f39f813242aea7d57c7410cf1
the_equality: more careful use of addSIs and addIs

diff -r 436019ca97d7 -r 3054a10ed5b5 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Nov 24 10:23:41 1994 +0100
+++ b/src/ZF/upair.ML	Thu Nov 24 10:31:47 1994 +0100
@@ -171,9 +171,9 @@
 
 val the_equality = prove_goalw ZF.thy [the_def]
     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
- (fn prems=>
-  [ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems) 
-	                 addEs (prems RL [subst])) 1) ]);
+ (fn [pa,eq] =>
+  [ (fast_tac (lemmas_cs addSIs [singletonI,pa] addIs [equalityI]
+	                 addEs [eq RS subst]) 1) ]);
 
 (* Only use this if you already know EX!x. P(x) *)
 val the_equality2 = prove_goal ZF.thy