diff -r 4b32a46ffd29 -r 168dbdaedb71 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 17:49:46 2001 +0200
@@ -89,7 +89,7 @@
 
 lemma Impl_sound_lemma: 
 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
-M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
+Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
 by blast
 
 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"