equal
deleted
inserted
replaced
670 |
670 |
671 ML {* |
671 ML {* |
672 fun included i bcs = |
672 fun included i bcs = |
673 let |
673 let |
674 fun incl (BEmy j) = i = j |
674 fun incl (BEmy j) = i = j |
675 | incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) |
675 | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) |
676 | incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) |
676 | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) |
677 | incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) |
677 | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) |
678 in |
678 in |
679 exists incl bcs |
679 exists incl bcs |
680 end |
680 end |
681 *} |
681 *} |
682 |
682 |