prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as proposed by Pedro Sánchez Terraf;

--- a/src/ZF/Constructible/AC_in_L.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -460,7 +460,7 @@
 apply (blast dest!: well_ord_L_r intro: well_ord_subset)
 done
 
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
 proof 
@@ -469,7 +469,7 @@
   then obtain r where "well_ord(x,r)" 
     by (blast dest: L_implies_AC) 
   thus "\<exists>r. wellordered(L,x,r)" 
-    by (blast intro: well_ord_imp_relativized)
+    by (blast intro: L.well_ord_imp_relativized)
 qed
 
 text\<open>In order to prove \<^term>\<open> \<exists>r[L]. wellordered(L,x,r)\<close>, it's necessary to know 

--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -581,7 +581,7 @@
     ==> transrec_replacement(L, \<lambda>x f u. 
               \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
                      big_union(L, r, u), j)"
-apply (rule transrec_replacementI, assumption)
+apply (rule L.transrec_replacementI, assumption)
 apply (unfold transrec_body_def)  
 apply (rule strong_replacementI)
 apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 

--- a/src/ZF/Constructible/L_axioms.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -110,7 +110,7 @@
    apply (rule Union_ax)
   done
 
-interpretation L?: M_trivial L by (rule M_trivial_L)
+interpretation L: M_trivial L by (rule M_trivial_L)
 
 (* Replaces the following declarations...
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]

--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -184,7 +184,7 @@
 theorem M_trancl_L: "M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
-interpretation L?: M_trancl L by (rule M_trancl_L)
+interpretation L: M_trancl L by (rule M_trancl_L)
 
 
 subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>list\<close>\<close>
@@ -371,7 +371,7 @@
   apply (rule M_datatypes_axioms_L) 
   done
 
-interpretation L?: M_datatypes L by (rule M_datatypes_L)
+interpretation L: M_datatypes L by (rule M_datatypes_L)
 
 
 subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>eclose\<close>\<close>
@@ -434,7 +434,7 @@
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation L?: M_eclose L by (rule M_eclose_L)
+interpretation L: M_eclose L by (rule M_eclose_L)
 
 
 end

--- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -961,11 +961,11 @@
 lemma formula_rec_replacement: 
       \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
    "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
-apply (rule transrec_replacementI, simp add: nat_into_M) 
+apply (rule L.transrec_replacementI, simp add: L.nat_into_M)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
          in gen_separation_multi [OF formula_rec_replacement_Reflects],
-       auto simp add: nat_into_M)
+       auto simp add: L.nat_into_M)
 apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
 done

--- a/src/ZF/Constructible/Separation.thy	Wed Mar 18 17:29:20 2020 +0100
+++ b/src/ZF/Constructible/Separation.thy	Wed Mar 18 17:44:27 2020 +0100
@@ -304,7 +304,7 @@
 theorem M_basic_L: " M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 
 end