# HG changeset patch
# User haftmann
# Date 1632481458 0
# Node ID 690928dd6f8fe71978c66c4731a9ef2c531625d7
# Parent  9e71155e36666cf5fa6bbdc7462c08ec77d2daa1
apply declarations from interpretations in eigen context also

diff -r 9e71155e3666 -r 690928dd6f8f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Sep 24 11:04:18 2021 +0000
@@ -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 =