src/ZF/upair.ML
changeset 738 3054a10ed5b5
parent 686 be908d8d41ef
child 760 f0200e91b272
--- 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