--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed May 05 18:25:34 2010 +0200
@@ -554,9 +554,9 @@
(* test for finiteness of domain definitions *)
local
val types = [@{type_name ssum}, @{type_name sprod}];
- fun finite d T = if T mem absTs then d else finite' d T
+ fun finite d T = if member (op =) absTs T then d else finite' d T
and finite' d (Type (c, Ts)) =
- let val d' = d andalso c mem types;
+ let val d' = d andalso member (op =) types c;
in forall (finite d') Ts end
| finite' d _ = true;
in