--- a/Nominal-General/nominal_eqvt.ML	Thu May 06 14:13:35 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Thu May 06 14:13:45 2010 +0200
@@ -77,7 +77,7 @@
 let
   fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
       (case head_of f1 of
-         Const (name, _) => if name mem names then SOME f2 else NONE
+         Const (name, _) => if member (op =) names name then SOME f2 else NONE
        | _ => NONE)
   | split_conj _ _ = NONE;
 in
@@ -178,4 +178,4 @@
       K.thy_decl (P.xname >> equivariance);
 end;
 
-end (* structure *)
\ No newline at end of file
+end (* structure *)

--- a/Nominal-General/nominal_permeq.ML	Thu May 06 14:13:35 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Thu May 06 14:13:45 2010 +0200
@@ -117,7 +117,7 @@
     let
       val hd = head_of trm
     in 
-      if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+      if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then ()
       else (if strict_flag then error else warning) 
              ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
     end
@@ -183,4 +183,4 @@
 fun perm_strict_simp_meth (thms, consts) ctxt = 
   SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
 
-end; (* structure *)
\ No newline at end of file
+end; (* structure *)

--- a/Nominal/Equivp.thy	Thu May 06 14:13:35 2010 +0200
+++ b/Nominal/Equivp.thy	Thu May 06 14:13:45 2010 +0200
@@ -56,7 +56,7 @@
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
-       add_0_left supp_zero_perm Int_empty_left split_conv})
+       add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps})
 *}
 
 ML {*
@@ -291,7 +291,7 @@
 ML {*
 fun choose_alpha_abs eqiff =
 let
-  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+  fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true;
   val terms = map prop_of eqiff;
   fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
   val no =

--- a/Nominal/NewFv.thy	Thu May 06 14:13:35 2010 +0200
+++ b/Nominal/NewFv.thy	Thu May 06 14:13:45 2010 +0200
@@ -140,7 +140,7 @@
   val non_rec_vars =
     case binds of
       [(SOME bn, i)] =>
-        if i mem bodys
+        if member (op =) bodys i
         then noatoms
         else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
     | _ => noatoms

--- a/Nominal/Rsp.thy	Thu May 06 14:13:35 2010 +0200
+++ b/Nominal/Rsp.thy	Thu May 06 14:13:45 2010 +0200
@@ -63,7 +63,7 @@
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps}))
   ))
 *}