--- a/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy
+++ b/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy
@@ -1,11 +1,13 @@
 header {* Locally Nameless representation of basic Sigma calculus enriched with formal parameter *}
 
-theory Sigma imports "../preliminary/FMap" begin
+theory Sigma
+imports "../preliminary/FMap"
+begin
 
 subsection {* Infrastructure for the finite maps *}
-consts max_label :: nat
-
-axioms LabelAvail: "max_label > 10"
+
+axiomatization max_label :: nat where
+  LabelAvail: "max_label > 10"
 
 typedef Label = "{n :: nat. n \<le> max_label}"
   by auto
@@ -2299,7 +2301,7 @@
   shows 
   "\<forall>k \<le> (card (dom f)). 
     (\<exists>ob. length ob = (k + 1)
-        \<and> (\<forall>obi. obi mem ob \<longrightarrow> dom (fst(obi)) = dom f \<and> ((snd obi) \<subseteq> dom f)) 
+        \<and> (\<forall>obi. obi \<in> set ob \<longrightarrow> dom (fst(obi)) = dom f \<and> ((snd obi) \<subseteq> dom f)) 
         \<and> (fst (ob!0) = f)
         \<and> (card (snd (ob!k)) = k)
         \<and> (\<forall>i < k. snd (ob!i) \<subset> snd (ob!k))
@@ -2312,7 +2314,7 @@
   show 
     "k \<le> card (dom f) 
     \<longrightarrow> (\<exists>ob. length ob = k + 1 
-            \<and> (\<forall>obi. obi mem ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f) 
+            \<and> (\<forall>obi. obi \<in> set ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f) 
             \<and> fst (ob ! 0) = f 
             \<and> card (snd (ob ! k)) = k 
             \<and> (\<forall>i<k. snd (ob ! i) \<subset> snd (ob ! k)) 
@@ -2330,7 +2332,7 @@
       with Suc.hyps
       obtain ob where 
 	"length ob = k + 1" and
-	mem_ob: "\<forall>obi. obi mem ob 
+	mem_ob: "\<forall>obi. obi \<in> set ob 
 	          \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f" and
 	"fst (ob ! 0) = f" and
 	"card (snd (ob ! k)) = k" and
@@ -2340,7 +2342,7 @@
 	         \<longrightarrow> Ltake_eq (snd (ob ! k)) (fst (ob ! k)) g 
 	             \<and> Ltake_eq (dom f - snd (ob ! k)) (fst (ob ! k)) f"
 	by auto
-      from `length ob = k + 1` have obkmem: "(ob!k) mem ob" by auto
+      from `length ob = k + 1` have obkmem: "(ob!k) \<in> set ob" by auto
 
       with mem_ob have obksnd: "snd(ob!k) \<subseteq> dom f" by blast
       from 
@@ -2377,15 +2379,15 @@
 
 	(* prop#2 *)
       moreover
-      have "\<forall>obi. obi mem ob' \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f"
+      have "\<forall>obi. obi \<in> set ob' \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f"
 	unfolding ob'_def
       proof (intro strip)
 	fix obi :: "(Label -~> sterm) \<times> (Label \<Rightarrow> bool)"
-	assume "obi mem ob @ [(fst(ob!k)(l' \<mapsto> the (g l')), insert l' (snd (ob!k)))]"
+	assume "obi \<in> set (ob @ [(fst(ob!k)(l' \<mapsto> the (g l')), insert l' (snd (ob!k)))])"
 	note mem_append_lem'[OF this]
 	thus "dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f"
 	proof (rule disjE, simp_all)
-	  assume "obi mem ob" 
+	  assume "obi \<in> set ob" 
 	  with mem_ob show "dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f"
 	    by blast
 	next
@@ -2518,7 +2520,7 @@
       ultimately
       show 
 	"\<exists>ob. length ob = Suc k + 1 
-	    \<and> (\<forall>obi. obi mem ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f) 
+	    \<and> (\<forall>obi. obi \<in> set ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f) 
 	    \<and> fst (ob ! 0) = f 
 	    \<and> card (snd (ob ! Suc k)) = Suc k 
 	    \<and> (\<forall>i<Suc k. snd (ob ! i) \<subset> snd (ob ! Suc k)) 
@@ -2548,14 +2550,14 @@
   obtain ob :: "((Label -~> sterm) \<times> (Label \<Rightarrow> bool)) list" 
     where 
     "length ob = card(dom f) + 1" and
-    "\<forall>obi. obi mem ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f" and
+    "\<forall>obi. obi \<in> set ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f" and
     "fst(ob!0) = f" and
     "card (snd(ob!card(dom f))) = card(dom f)" and
     "Obj (fst(ob!0)) T \<rightarrow>\<^sub>\<beta>\<^sup>* Obj (fst(ob!card(dom f))) T" and
     "Ltake_eq (snd(ob!card(dom f))) (fst(ob!card(dom f))) g"
     by blast
-  from `length ob = card (dom f) + 1` have "(ob!card(dom f)) mem ob" by auto
-  with `\<forall>obi. obi mem ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f`
+  from `length ob = card (dom f) + 1` have "(ob!card(dom f)) \<in> set ob" by auto
+  with `\<forall>obi. obi \<in> set ob \<longrightarrow> dom (fst obi) = dom f \<and> snd obi \<subseteq> dom f`
   have "dom (fst(ob!card(dom f))) = dom f" and "snd(ob!card(dom f)) \<subseteq> dom f"
     by blast+