# HG changeset patch
# User wenzelm
# Date 1537784179 -7200
# Node ID 812e60d15172ede19a93ffead7a2aea3cf66581d
# Parent  1ad2897ba24432c48404211da8075bc58a5124ce
clarified signature;

diff -r 1ad2897ba244 -r 812e60d15172 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Sep 24 12:07:17 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Mon Sep 24 12:16:19 2018 +0200
@@ -163,13 +163,16 @@
 
 (* interpretation in local theories *)
 
+fun activate_fragment registration =
+  Local_Theory.mark_brittle #> Locale.add_registration_local_theory registration;
+
 fun interpretation expression =
   generic_interpretation cert_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Locale.activate_fragment expression [];
+    Local_Theory.notes_kind activate_fragment expression [];
 
 fun interpretation_cmd expression =
   generic_interpretation read_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Locale.activate_fragment expression [];
+    Local_Theory.notes_kind activate_fragment expression [];
 
 
 (* interpretation into global theories *)
@@ -226,7 +229,7 @@
 fun register_or_activate lthy =
   if Named_Target.is_theory lthy
   then Local_Theory.theory_registration
-  else Locale.activate_fragment;
+  else activate_fragment;
 
 fun gen_isar_interpretation prep_interpretation expression lthy =
   generic_interpretation prep_interpretation Element.witness_proof_eqs
diff -r 1ad2897ba244 -r 812e60d15172 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 12:07:17 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 12:16:19 2018 +0200
@@ -81,7 +81,6 @@
   val add_registration_theory: registration -> theory -> theory
   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 registrations_of: Context.generic -> string -> (string * morphism) list
   val add_dependency: string -> registration -> theory -> theory
 
@@ -574,12 +573,6 @@
   end;
 
 
-(* locale fragments within local theory *)
-
-fun activate_fragment registration =
-  Local_Theory.mark_brittle #> add_registration_local_theory registration;
-
-
 
 (*** Dependencies ***)