--- a/src/Pure/Isar/locale.ML Fri Dec 18 10:37:26 2020 +0000
+++ b/src/Pure/Isar/locale.ML Sat Dec 19 09:33:11 2020 +0000
@@ -615,16 +615,13 @@
val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
-fun add_registration_local_theory' registration lthy =
+fun add_registration_local_theory registration lthy =
let val n = Local_Theory.level lthy in
lthy
|> Local_Theory.map_contexts (fn level =>
level = n - 1 ? Context.proof_map (add_registration registration))
end;
-fun add_registration_local_theory registration =
- Local_Theory.revoke_reinitializability #> add_registration_local_theory' registration
-
fun add_registration_proof registration ctxt = ctxt
|> Proof_Context.set_stmt false
|> Context.proof_map (add_registration registration)
@@ -658,7 +655,7 @@
fun add_dependency loc registration =
Local_Theory.raw_theory (add_dependency' loc registration)
- #> add_registration_local_theory' registration;
+ #> add_registration_local_theory registration;
(*** Storing results ***)