# HG changeset patch
# User wenzelm
# Date 1632516253 -7200
# Node ID 383fd113baaef48b89f6d29f0efd0873d491fc44
# Parent  690928dd6f8fe71978c66c4731a9ef2c531625d7# Parent  0135a0c77b64e75eff1f5ddc4f4ea211001cfd1e
merged

diff -r 0135a0c77b64 -r 383fd113baae src/Pure/Isar/generic_target.ML
--- 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 =