src/HOL/Nominal/nominal_inductive.ML
changeset 36692 54b64d4ad524
parent 36428 874843c1e96e
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  fun mk_perm_bool_simproc names = Simplifier.simproc_i
     1.5    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
     1.6      fn Const ("Nominal.perm", _) $ _ $ t =>
     1.7 -         if the_default "" (try (head_of #> dest_Const #> fst) t) mem names
     1.8 +         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
     1.9           then SOME perm_bool else NONE
    1.10       | _ => NONE);
    1.11  
    1.12 @@ -73,7 +73,7 @@
    1.13  
    1.14  fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
    1.15        Const (name, _) =>
    1.16 -        if name mem names then SOME (f p q) else NONE
    1.17 +        if member (op =) names name then SOME (f p q) else NONE
    1.18      | _ => NONE)
    1.19    | split_conj _ _ _ _ = NONE;
    1.20  
    1.21 @@ -92,7 +92,7 @@
    1.22  fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
    1.23        (case head_of p of
    1.24           Const (name, _) =>
    1.25 -           if name mem names then SOME (HOLogic.mk_conj (p,
    1.26 +           if member (op =) names name then SOME (HOLogic.mk_conj (p,
    1.27               Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
    1.28                 (subst_bounds (pis, strip_all pis q))))
    1.29             else NONE
    1.30 @@ -214,7 +214,7 @@
    1.31      fun lift_prem (t as (f $ u)) =
    1.32            let val (p, ts) = strip_comb t
    1.33            in
    1.34 -            if p mem ps then
    1.35 +            if member (op =) ps p then
    1.36                Const (inductive_forall_name,
    1.37                  (fsT --> HOLogic.boolT) --> HOLogic.boolT) $
    1.38                    Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    1.39 @@ -510,7 +510,7 @@
    1.40                    val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
    1.41                    val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
    1.42                       (fn x as Free _ =>
    1.43 -                           if x mem args then x
    1.44 +                           if member (op =) args x then x
    1.45                             else (case AList.lookup op = tab x of
    1.46                               SOME y => y
    1.47                             | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)