src/ZF/InfDatatype.ML
changeset 768 59c0a821e468
parent 760 f0200e91b272
child 801 316121afb5b5
--- a/src/ZF/InfDatatype.ML	Thu Dec 08 14:06:16 1994 +0100
+++ b/src/ZF/InfDatatype.ML	Thu Dec 08 14:18:31 1994 +0100
@@ -176,7 +176,7 @@
 val le_nat_Un_cardinal = 
     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
 
-val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
+val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le 
                         |> standard;
 
 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)