diff -r 2a2a86b57fed -r 3a05a7f549bd src/ZF/Cardinal.ML
--- 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);