merged

--- a/src/Pure/Isar/generic_target.ML	Fri Sep 24 22:23:26 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Sep 24 22:44:13 2021 +0200
@@ -243,7 +243,7 @@
     then Context.proof_map (Locale.add_registration registration)
     else I) lthy;
 
-val local_interpretation = standard_registration (fn (n, level) => level = n - 1);
+val local_interpretation = standard_registration (fn (n, level) => level >= n - 1);
 
 
 
@@ -413,6 +413,7 @@
             Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
 
+
 (** theory operations **)
 
 val theory_abbrev = abbrev theory_target_abbrev;
@@ -431,6 +432,7 @@
   |> standard_registration (K true) registration;
 
 
+
 (** locale target primitives **)
 
 fun locale_target_notes locale kind global_facts local_facts =