--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 17:21:48 2009 +0100
@@ -1928,7 +1928,8 @@
{ fix t n assume tnY: "(t,n) \<in> set ?Y"
hence "(t,n) \<in> set ?SS" by simp
hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
- by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
+ by (auto simp add: split_def simp del: map_map)
+ (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
from simp_num_pair_l[OF tnb np tns]