--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Jun 06 19:12:59 2007 +0200
@@ -48,7 +48,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') \<in> ps. p'=p] ++_f ss!p"
+ (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp