src/HOL/Nominal/nominal_datatype.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5  fun mk_case_names_exhausts descr new =
     1.6    map (Rule_Cases.case_names o exhaust_cases descr o #1)
     1.7 -    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
     1.8 +    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -131,7 +131,7 @@
    1.13        let
    1.14          val (aT as Type (a, []), S) = dest_permT T;
    1.15          val (bT as Type (b, []), _) = dest_permT U
    1.16 -      in if aT mem permTs_of u andalso aT <> bT then
    1.17 +      in if member (op =) (permTs_of u) aT andalso aT <> bT then
    1.18            let
    1.19              val cp = cp_inst_of thy a b;
    1.20              val dj = dj_thm_of thy b a;
    1.21 @@ -1772,7 +1772,7 @@
    1.22                      val params' = params1 @ params2;
    1.23                      val rec_prems = filter (fn th => case prop_of th of
    1.24                          _ $ p => (case head_of p of
    1.25 -                          Const (s, _) => s mem rec_set_names
    1.26 +                          Const (s, _) => member (op =) rec_set_names s
    1.27                          | _ => false)
    1.28                        | _ => false) prems';
    1.29                      val fresh_prems = filter (fn th => case prop_of th of