diff -r 67110d6c66de -r 66c68453455c src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 15:18:52 2011 +0100
@@ -99,17 +99,18 @@
 
 subsection "Fully polymorphic variants, required for Example only"
 
-axioms
-
+axiomatization where
   Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
              \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                  A \<turnstile> {P} c {Q }"
 
- eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
+axiomatization where
+  eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
              \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
                  A \<turnstile>\<^sub>e {P} e {Q }"
 
- Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
+axiomatization where
+  Impl: "\<forall>Z. 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 ==>
                     A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"