--- 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 =