src/Pure/Isar/locale.ML

   val amend_registration: registration -> Context.generic -> Context.generic
   val add_registration: registration -> Context.generic -> Context.generic
   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
 
   (* Diagnostic *)
   val get_locales: theory -> string list

     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 #> add_registration_local_theory registration;
-
-
 
 (*** Dependencies ***)
 
 fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   let