# HG changeset patch
# User wenzelm
# Date 877001908 -7200
# Node ID 04f730731e43a163274b97d6bb779a7e3dbbab9b
# Parent  eb0681305d3fe521894b3db36719e9552fcfe18a
transfer CardinalArith.thy nat_into_Ord;

diff -r eb0681305d3f -r 04f730731e43 src/ZF/CardinalArith.ML
--- 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);