--- a/src/Tools/permanent_interpretation.ML Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML Fri Apr 25 21:45:04 2014 +0200
@@ -85,13 +85,8 @@
(* interpretation with permanent registration *)
-fun subscribe lthy =
- if Named_Target.is_theory lthy
- then Generic_Target.theory_registration
- else Generic_Target.locale_dependency (Named_Target.the_name lthy);
-
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
- generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
+ generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.subscription
expression raw_defs raw_eqns lthy
in