src/Pure/Isar/interpretation.ML

 fun setup_proof state after_qed propss eqns goal_ctxt =
   Element.witness_local_proof_eqs
     (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     "interpret" propss eqns goal_ctxt state;
 
+fun add_registration_proof registration ctxt = ctxt
+  |> Proof_Context.set_stmt false
+  |> Context.proof_map (Locale.add_registration registration)
+  |> Proof_Context.restore_stmt ctxt;
+
 fun gen_interpret prep_interpretation expression state =
   Proof.assert_forward_or_chain state
   |> Proof.context_of
   |> generic_interpretation prep_interpretation (setup_proof state)
-    Attrib.local_notes Locale.add_registration_proof expression [];
+    Attrib.local_notes add_registration_proof expression [];
 
 in
 
 val interpret = gen_interpret cert_interpretation;
 val interpret_cmd = gen_interpret read_interpretation;

 
 
 (* interpretation in local theories *)
 
 val add_registration_local_theory =
-  Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+  Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation;
 
 fun interpretation expression =
   generic_interpretation cert_interpretation Element.witness_proof_eqs
     Local_Theory.notes_kind add_registration_local_theory expression [];