src/HOLCF/Tools/Domain/domain_take_proofs.ML
changeset 36692 54b64d4ad524
parent 36241 2a4cec6bcae2
child 37078 a1656804fcad
     1.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -554,9 +554,9 @@
     1.4      (* test for finiteness of domain definitions *)
     1.5      local
     1.6        val types = [@{type_name ssum}, @{type_name sprod}];
     1.7 -      fun finite d T = if T mem absTs then d else finite' d T
     1.8 +      fun finite d T = if member (op =) absTs T then d else finite' d T
     1.9        and finite' d (Type (c, Ts)) =
    1.10 -          let val d' = d andalso c mem types;
    1.11 +          let val d' = d andalso member (op =) types c;
    1.12            in forall (finite d') Ts end
    1.13          | finite' d _ = true;
    1.14      in