diff -r 458b4e3720ab -r 27f3c10b0b50 src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/Mutex.thy	Mon Dec 07 10:23:50 2015 +0100
@@ -27,7 +27,7 @@
 abbreviation "u == Var([0,1])"
 abbreviation "v == Var([1,0])"
 
-axiomatization where --\<open>* Type declarations  *\<close>
+axiomatization where \<comment>\<open>* Type declarations  *\<close>
   p_type:  "type_of(p)=bool & default_val(p)=0" and
   m_type:  "type_of(m)=int  & default_val(m)=#0" and
   n_type:  "type_of(n)=int  & default_val(n)=#0" and