diff -r b85c62c4e826 -r 6003b4f916c0 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Mon Feb 25 11:27:07 2002 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Feb 25 18:02:22 2002 +0100
@@ -113,9 +113,10 @@
             A |-e {P} e {Q }"
 
 
-subsection "Fully polymorphic variants"
+subsection "Fully polymorphic variants, required for Example only"
 
 axioms
+
   Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
              \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                  A |- {P} c {Q }"
@@ -202,11 +203,11 @@
 by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
 lemma Impl1': 
-   "\<lbrakk>\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
+   "\<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 Impl)
+apply (drule AxSem.Impl)
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)
 done