# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265301544 -3600
# Node ID b93b631570ca773171c683bfb245eab5fb58b923
# Parent  dfea9e73923190df791d0d4ba5db808be6172d11
fixed (permute_eqvt in eqvts makes this simpset always looping)

diff -r dfea9e739231 -r b93b631570ca Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Thu Feb 04 15:19:24 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Feb 04 17:39:04 2010 +0100
@@ -29,7 +29,7 @@
 apply(auto)
 apply(drule_tac x="p \<bullet> xa" in bspec)
 apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
+apply(simp add: eqvts del: permute_eqvt)
 apply(simp add: fresh_permute_iff)
 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
 apply(simp)