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