diff -r 4b32a46ffd29 -r 168dbdaedb71 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 17:49:46 2001 +0200
@@ -88,9 +88,9 @@
 
   (*\<Union>z instead of \<forall>z in the conclusion and
       z restricted to type state due to limitations of the inductive package *)
-  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- 
-                            (\<lambda>M. (P z M, body M, Q z M))`Ms ==>
-                      A ||- (\<lambda>M. (P z M, Impl M, Q z M))`Ms"
+  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- 
+                            (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
+                      A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
 
 (* structural rules *)
 
@@ -148,10 +148,10 @@
 by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
 lemma Impl1: 
-   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) |\<turnstile> 
-                        (\<lambda>M. (P z M, body M, Q z M))`Ms; 
-    M \<in> Ms\<rbrakk> \<Longrightarrow> 
-                A         \<turnstile>  {P z M} Impl M {Q z M}"
+   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) |\<turnstile> 
+                        (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms; 
+    Cm \<in> Ms\<rbrakk> \<Longrightarrow> 
+                A         \<turnstile>  {P z Cm} Impl Cm {Q z Cm}"
 apply (drule hoare_ehoare.Impl)
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)