# HG changeset patch
# User lcp
# Date 786892711 -3600
# Node ID 59c0a821e4688d9ba6c7855a36220d4afc11b986
# Parent  a4fce3b940659569722c92222d03bbe74bde815b
UN_upper_cardinal: updated to refer to Card_le_imp_lepoll
and lepoll_imp_Card_le

diff -r a4fce3b94065 -r 59c0a821e468 src/ZF/InfDatatype.ML
--- 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)) *)