--- a/src/Pure/Isar/interpretation.ML Fri Dec 18 10:37:26 2020 +0000
+++ b/src/Pure/Isar/interpretation.ML Sat Dec 19 09:33:11 2020 +0000
@@ -156,13 +156,16 @@
(* interpretation in local theories *)
+val add_registration_local_theory =
+ Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
fun interpretation_cmd expression =
generic_interpretation read_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
(* interpretation into global theories *)
@@ -219,7 +222,7 @@
fun register_or_activate lthy =
if Named_Target.is_theory lthy
then Local_Theory.theory_registration
- else Locale.add_registration_local_theory;
+ else add_registration_local_theory;
fun gen_isar_interpretation prep_interpretation expression lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs