# HG changeset patch
# User wenzelm
# Date 1535631039 -7200
# Node ID becaeaa334aef3a887186f9ddc066ad45d4f93cf
# Parent  6c9825c1e26b144ebed2029536b9057719f22372
clarified signature;

diff -r 6c9825c1e26b -r becaeaa334ae src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 13:38:52 2018 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:10:39 2018 +0200
@@ -406,7 +406,7 @@
 
 fun locale_dependency locale registration =
   Local_Theory.raw_theory (Locale.add_dependency locale registration)
-  #> Locale.activate_fragment_nonbrittle registration;
+  #> Locale.add_registration_local_theory registration;
 
 
 (** locale abbreviations **)
diff -r 6c9825c1e26b -r becaeaa334ae src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 13:38:52 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:10:39 2018 +0200
@@ -153,16 +153,11 @@
     (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     "interpret" propss eqns goal_ctxt state;
 
-fun add_registration 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 add_registration expression [];
+    Attrib.local_notes Locale.add_registration_proof expression [];
 
 in
 
diff -r 6c9825c1e26b -r becaeaa334ae src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 30 13:38:52 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:10:39 2018 +0200
@@ -76,8 +76,9 @@
   type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
   val amend_registration: registration -> Context.generic -> Context.generic
   val add_registration: registration -> Context.generic -> Context.generic
+  val add_registration_proof: registration -> Proof.context -> Proof.context
+  val add_registration_local_theory: registration -> local_theory -> local_theory
   val activate_fragment: registration -> local_theory -> local_theory
-  val activate_fragment_nonbrittle: registration -> local_theory -> local_theory
   val registrations_of: Context.generic -> string -> (string * morphism) list
   val add_dependency: string -> registration -> theory -> theory
 
@@ -558,17 +559,23 @@
       |> activate_facts (SOME export) (name, morph)
   end;
 
+fun add_registration_proof registration ctxt = ctxt
+  |> Proof_Context.set_stmt false
+  |> Context.proof_map (add_registration registration)
+  |> Proof_Context.restore_stmt ctxt;
 
-(* locale fragments within local theory *)
 
-fun activate_fragment_nonbrittle 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;
 
+
+(* locale fragments within local theory *)
+
 fun activate_fragment registration =
-  Local_Theory.mark_brittle #> activate_fragment_nonbrittle registration;
+  Local_Theory.mark_brittle #> add_registration_local_theory registration;