clarified name

--- a/src/Pure/Isar/local_theory.ML	Sat Dec 19 00:23:21 2020 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Dec 18 10:37:26 2020 +0000
@@ -24,7 +24,7 @@
   type operations
   val assert: local_theory -> local_theory
   val level: Proof.context -> int
-  val mark_brittle: local_theory -> local_theory
+  val revoke_reinitializability: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val background_naming_of: local_theory -> Name_Space.naming
   val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -69,7 +69,7 @@
     conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
-  val exit_global_nonbrittle: local_theory -> theory
+  val exit_global_reinitializable: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
   val begin_nested: local_theory -> Binding.scope * local_theory
@@ -105,12 +105,12 @@
  {background_naming: Name_Space.naming,
   operations: operations,
   conclude: Proof.context -> Proof.context,
-  brittle: bool,
+  reinitializable: bool,
   target: Proof.context};
 
-fun make_lthy (background_naming, operations, conclude, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, conclude, reinitializable, target) : lthy =
   {background_naming = background_naming, operations = operations,
-    conclude = conclude, brittle = brittle, target = target};
+    conclude = conclude, reinitializable = reinitializable, target = target};
 
 
 (* context data *)
@@ -150,16 +150,16 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {background_naming, operations, conclude, brittle, target} :: parents =>
-    make_lthy (f (background_naming, operations, conclude, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, conclude, reinitializable, target} :: parents =>
+    make_lthy (f (background_naming, operations, conclude, reinitializable, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
-      (fn (i, {background_naming, operations, conclude, brittle, target}) =>
-        make_lthy (background_naming, operations, conclude, brittle,
+      (fn (i, {background_naming, operations, conclude, reinitializable, target}) =>
+        make_lthy (background_naming, operations, conclude, reinitializable,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
@@ -168,17 +168,17 @@
   end;
 
 
-(* brittle context -- implicit for nested structures *)
+(* reinitializable context -- implicit for nested structures *)
 
-fun mark_brittle lthy =
+fun revoke_reinitializability lthy =
   if level lthy = 1 then
     map_top (fn (background_naming, operations, conclude, _, target) =>
-      (background_naming, operations, conclude, true, target)) lthy
+      (background_naming, operations, conclude, false, target)) lthy
   else lthy;
 
-fun assert_nonbrittle lthy =
-  if #brittle (top_of lthy) then error "Brittle local theory context"
-  else lthy;
+fun assert_reinitializable lthy =
+  if #reinitializable (top_of lthy) then lthy
+  else error "Non-reinitializable local theory context";
 
 
 (* naming for background theory *)
@@ -186,8 +186,8 @@
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
-  map_top (fn (background_naming, operations, conclude, brittle, target) =>
-    (f background_naming, operations, conclude, brittle, target));
+  map_top (fn (background_naming, operations, conclude, reinitializable, target) =>
+    (f background_naming, operations, conclude, reinitializable, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
@@ -354,7 +354,7 @@
 
 fun init_target background_naming conclude operations target =
   Data.map (K [make_lthy
-    (background_naming, operations, conclude, false, target)]) target
+    (background_naming, operations, conclude, true, target)]) target
 
 fun init {background_naming, setup, conclude} operations thy =
   thy
@@ -366,7 +366,7 @@
 
 fun exit lthy = exit_of lthy (assert_bottom lthy);
 val exit_global = Proof_Context.theory_of o exit;
-val exit_global_nonbrittle = exit_global o assert_nonbrittle;
+val exit_global_reinitializable = exit_global o assert_reinitializable;
 
 fun exit_result decl (x, lthy) =
   let

--- a/src/Pure/Isar/locale.ML	Sat Dec 19 00:23:21 2020 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 18 10:37:26 2020 +0000
@@ -623,7 +623,7 @@
   end;
 
 fun add_registration_local_theory registration =
-  Local_Theory.mark_brittle #> add_registration_local_theory' registration
+  Local_Theory.revoke_reinitializability #> add_registration_local_theory' registration
 
 fun add_registration_proof registration ctxt = ctxt
   |> Proof_Context.set_stmt false

--- a/src/Pure/Isar/named_target.ML	Sat Dec 19 00:23:21 2020 +0100
+++ b/src/Pure/Isar/named_target.ML	Fri Dec 18 10:37:26 2020 +0000
@@ -125,7 +125,7 @@
         setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes,
         conclude = I}
        (operations target)
-    |> not (null includes) ? Local_Theory.mark_brittle
+    |> not (null includes) ? Local_Theory.revoke_reinitializability
   end;
 
 val theory_init = init [] "";

--- a/src/Pure/Isar/target_context.ML	Sat Dec 19 00:23:21 2020 +0100
+++ b/src/Pure/Isar/target_context.ML	Fri Dec 18 10:37:26 2020 +0000
@@ -37,7 +37,7 @@
       (Context.Proof o Local_Theory.reset, lthy)
   | switch_named_cmd (SOME name) (Context.Proof lthy) =
       (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
-        (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy);
+        (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy);
 
 fun includes raw_includes lthy =
   Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;