# HG changeset patch
# User paulson
# Date 847458171 -3600
# Node ID 5819e85ad261928ba6deeca52d347481805c9583
# Parent  d276a806cc101357c8808c13159361373c8e1264
Adjusting to new version of uresult

diff -r d276a806cc10 -r 5819e85ad261 src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Thu Nov 07 10:19:15 1996 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Fri Nov 08 14:02:51 1996 +0100
@@ -31,9 +31,8 @@
 (* The case of infinite set                                               *)
 (* ********************************************************************** *)
 
-goal thy "!!x. well_ord(x,r) ==> well_ord({{y,z}. y:x},?s(x,z))";
-by (eresolve_tac [paired_bij RS bij_is_inj RS well_ord_rvimage] 1);
-val well_ord_paired = uresult();
+(* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z))  **)
+val well_ord_paired = standard (paired_bij RS bij_is_inj RS well_ord_rvimage);
 
 goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C";
 by (fast_tac (FOL_cs addEs [notE, lepoll_trans]) 1);
diff -r d276a806cc10 -r 5819e85ad261 src/ZF/AC/AC1_WO2.ML
--- a/src/ZF/AC/AC1_WO2.ML	Thu Nov 07 10:19:15 1996 +0100
+++ b/src/ZF/AC/AC1_WO2.ML	Fri Nov 08 14:02:51 1996 +0100
@@ -7,6 +7,7 @@
 
 open AC1_WO2;
 
+(*Establishing the existence of a bijection -- hence the need for uresult*)
 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
 \       ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
@@ -14,7 +15,7 @@
 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
 by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);
 by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);
-val lemma1 = uresult();
+val lemma1 = uresult() |> standard;
 
 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
 by (rtac allI 1);