src/Pure/Isar/locale.ML
changeset 69050 812e60d15172
parent 69049 1ad2897ba244
child 69051 3cda9402a22a
--- 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 ***)