# HG changeset patch
# User wenzelm
# Date 877002327 -7200
# Node ID 8b9f0bc6dc1aa780bae5ff8e1ba1cd8a672226ce
# Parent  5a1f22e7b359afaa0ddb616e9611f59c6b534943
oops;

diff -r 5a1f22e7b359 -r 8b9f0bc6dc1a src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Oct 16 13:45:16 1997 +0200
+++ b/src/ZF/Cardinal.ML	Thu Oct 16 13:45:27 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 [transfer thy Ord_nat RS Ord_in_Ord RS well_ord_Memre] 1);
+by (forward_tac [transfer thy Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
 by (rewtac well_ord_def);
 by (blast_tac (!claset addSIs [tot_ord_converse, 
 			       nat_wf_on_converse_Memrel]) 1);