# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273147796 -7200
# Node ID ff69913e2608e7883ac84ae378207b5dff761dc8
# Parent  2b6ba4d4e19ae5f6545a47181891af7ee0466807
prod_rel.simps and Fixed for new isabelle

diff -r 2b6ba4d4e19a -r ff69913e2608 Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Thu May 06 14:09:21 2010 +0200
+++ b/Nominal/Equivp.thy	Thu May 06 14:09:56 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 =