src/Pure/Isar/local_theory.ML

--- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 13:30:28 2014 +0200
@@ -7,6 +7,12 @@
 type local_theory = Proof.context;
 type generic_theory = Context.generic;
 
+structure Attrib =
+struct
+  type src = Args.src;
+  type binding = binding * src list;
+end;
+
 signature LOCAL_THEORY =
 sig
   type operations
@@ -14,6 +20,7 @@
   val restore: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: bool -> local_theory -> local_theory
+  val mark_brittle: local_theory -> local_theory
   val assert_nonbrittle: local_theory -> local_theory
   val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     local_theory -> local_theory
@@ -58,10 +65,6 @@
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val activate: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
@@ -307,17 +310,6 @@
 val const_alias = alias Sign.const_alias Proof_Context.const_alias;
 
 
-(* activation of locale fragments *)
-
-fun activate_nonbrittle dep_morph mixin export =
-  map_top (fn (naming, operations, after_close, brittle, target) =>
-    (naming, operations, after_close, brittle,
-      (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
-
-fun activate dep_morph mixin export =
-  mark_brittle #> activate_nonbrittle dep_morph mixin export;
-
-
 
 (** init and exit **)