src/Pure/Isar/local_theory.ML

   type operations
   val assert: local_theory -> local_theory
   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
   val close_target: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val naming_of: local_theory -> Name_Space.naming

 
 (* context data *)
 
 structure Data = Proof_Data
 (
-  type T = lthy list;
-  fun init _ = [];
+  type T = lthy list * bool;
+  fun init _ = ([], false);
 );
 
 fun assert lthy =
-  if null (Data.get lthy) then error "Missing local theory context" else lthy;
-
-val get_last_lthy = List.last o Data.get o assert;
-val get_first_lthy = hd o Data.get o assert;
+  if null (fst (Data.get lthy)) then error "Missing local theory context" else lthy;
+
+val get_last_lthy = List.last o fst o Data.get o assert;
+val get_first_lthy = hd o fst o Data.get o assert;
 
 fun map_first_lthy f =
   assert #>
-  Data.map (fn {naming, operations, after_close, target} :: parents =>
+  (Data.map o apfst) (fn {naming, operations, after_close, target} :: parents =>
     make_lthy (f (naming, operations, after_close, target)) :: parents);
 
-fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
+fun restore lthy = #target (get_first_lthy lthy) |> Data.put (fst (Data.get lthy), false);
 
 
 (* nested structure *)
 
-val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
+val level = length o fst o Data.get;  (*1: main target at bottom, >= 2: nested context*)
 
 fun assert_bottom b lthy =
   let
     val _ = assert lthy;
     val b' = level lthy <= 1;

     else lthy
   end;
 
 fun open_target naming operations after_close target =
   assert target
-  |> Data.map (cons (make_lthy (naming, operations, after_close, target)));
+  |> (Data.map o apfst) (cons (make_lthy (naming, operations, after_close, target)));
 
 fun close_target lthy =
   let
     val _ = assert_bottom false lthy;
-    val {after_close, ...} :: rest = Data.get lthy;
-  in lthy |> Data.put rest |> restore |> after_close end;
+    val ({after_close, ...} :: rest, tainted) = Data.get lthy;
+  in lthy |> Data.put (rest, tainted) |> restore |> after_close end;
 
 fun map_contexts f lthy =
   let val n = level lthy in
-    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, target}) =>
+    lthy |> (Data.map o apfst o map_index) (fn (i, {naming, operations, after_close, target}) =>
       make_lthy (naming, operations, after_close,
         target
         |> Context_Position.set_visible false
         |> f (n - i - 1)
         |> Context_Position.restore_visible target))
     |> f n
   end;
+
+
+(* brittle context -- implicit for nested structures *)
+
+val mark_brittle = Data.map (fn ([data], _) => ([data], true) | x => x);
+
+fun assert_nonbrittle lthy =
+  if snd (Data.get lthy) orelse level lthy > 1
+  then error "Brittle local theory context"
+  else lthy;
 
 
 (* naming *)
 
 val naming_of = #naming o get_first_lthy;

 (** init and exit **)
 
 (* init *)
 
 fun init naming operations target =
-  target |> Data.map
+  target |> (Data.map o apfst)
     (fn [] => [make_lthy (naming, operations, I, target)]
       | _ => error "Local theory already initialized")
   |> checkpoint;