src/HOL/Tools/refute.ML
changeset 36692 54b64d4ad524
parent 36555 8ff45c2076da
child 37117 59cee8807c29
     1.1 --- a/src/HOL/Tools/refute.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -463,7 +463,7 @@
     1.4    in
     1.5      (* I'm not quite sure if checking the name 's' is sufficient, *)
     1.6      (* or if we should also check the type 'T'.                   *)
     1.7 -    s mem_string class_const_names
     1.8 +    member (op =) class_const_names s
     1.9    end;
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 @@ -499,7 +499,7 @@
    1.13    in
    1.14      (* I'm not quite sure if checking the name 's' is sufficient, *)
    1.15      (* or if we should also check the type 'T'.                   *)
    1.16 -    s mem_string rec_names
    1.17 +    member (op =) rec_names s
    1.18    end;
    1.19  
    1.20  (* ------------------------------------------------------------------------- *)
    1.21 @@ -932,7 +932,7 @@
    1.22                | Datatype_Aux.DtType (_, ds) =>
    1.23                  collect_types dT (fold_rev collect_dtyp ds acc)
    1.24                | Datatype_Aux.DtRec i =>
    1.25 -                if dT mem acc then
    1.26 +                if member (op =) acc dT then
    1.27                    acc  (* prevent infinite recursion *)
    1.28                  else
    1.29                    let
    1.30 @@ -2248,7 +2248,7 @@
    1.31                            (* if 't_elem' existed at the previous depth,    *)
    1.32                            (* proceed recursively, otherwise map the entire *)
    1.33                            (* subtree to "undefined"                        *)
    1.34 -                          if t_elem mem terms' then
    1.35 +                          if member (op =) terms' t_elem then
    1.36                              make_constr ds off
    1.37                            else
    1.38                              (make_undef ds, off))