--- a/src/HOL/MicroJava/DFA/Kildall.thy Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Tue May 22 11:08:37 2018 +0200
@@ -38,7 +38,7 @@
lemma (in Semilat) nth_merges:
"\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
- (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
+ (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp