transfer thy Ord_nat;

--- a/src/ZF/AC/AC16_WO4.ML	Thu Oct 16 13:42:29 1997 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Oct 16 13:42:53 1997 +0200
@@ -55,7 +55,7 @@
 
 goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)";
 by (res_inst_tac [("x","{{a,x}. a:nat Un  Hartog(z)}")] exI 1);
-by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS
+by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS
                 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1);
 by (fast_tac (!claset addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired,
         equals0I, HartogI RSN (2, lepoll_trans1),

--- a/src/ZF/Cardinal.ML	Thu Oct 16 13:42:29 1997 +0200
+++ b/src/ZF/Cardinal.ML	Thu Oct 16 13:42:53 1997 +0200
@@ -754,7 +754,7 @@
 qed "nat_wf_on_converse_Memrel";
 
 goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))";
-by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
+by (forward_tac [transfer thy Ord_nat RS Ord_in_Ord RS well_ord_Memre] 1);
 by (rewtac well_ord_def);
 by (blast_tac (!claset addSIs [tot_ord_converse, 
 			       nat_wf_on_converse_Memrel]) 1);