transfer CardinalArith.thy nat_into_Ord;

--- a/src/ZF/CardinalArith.ML	Thu Oct 16 13:36:04 1997 +0200
+++ b/src/ZF/CardinalArith.ML	Thu Oct 16 13:38:28 1997 +0200
@@ -798,7 +798,8 @@
 
 (** Thanks to Krzysztof Grabczewski **)
 
-val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel;
+val nat_implies_well_ord =
+  (transfer CardinalArith.thy nat_into_Ord) RS well_ord_Memrel;
 
 goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
 by (rtac eqpoll_trans 1);