src/HOL/Decision_Procs/Ferrack.thy

   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
   proof-
     { 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]
       have "numbound0 t \<and> n > 0" . }
     thus ?thesis by blast