src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36837 4d1dd57103b9
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -292,7 +292,7 @@
     1.4         it has a possibly indirectly recursive argument that isn't/is possibly 
     1.5         indirectly lazy *)
     1.6      fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
     1.7 -          is_rec arg andalso not(rec_of arg mem ns) andalso
     1.8 +          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
     1.9            ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
    1.10              rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
    1.11                (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))