src/HOL/Nominal/nominal_inductive2.ML
changeset 36692 54b64d4ad524
parent 36428 874843c1e96e
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -46,7 +46,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 @@ -77,7 +77,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 @@ -96,7 +96,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 @@ -239,7 +239,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))