diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Fri Sep 21 18:23:15 2001 +0200
@@ -115,7 +115,7 @@
 apply (drule (1) eval_eval_max, erule thin_rl)
 by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
 
-lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body M-n\<rightarrow> t)"
+lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)"
 apply (rule ext)
 apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
 done