src/Pure/Isar/local_theory.ML

 
 signature LOCAL_THEORY =
 sig
   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 open_target: Name_Space.naming -> operations -> local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory

   val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
-  val restore: local_theory -> local_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory

 
 fun map_first_lthy f = assert #>
   Data.map (fn {naming, operations, target} :: parents =>
     make_lthy (f (naming, operations, target)) :: parents);
 
+fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
+
 
 (* nested structure *)
 
 val level = length o Data.get;
 

         |> map_contexts (K (Context.proof_map inherit))
         |> Context.Proof
       end
   | propagate_ml_env context = context;
 
-fun restore lthy = target_of lthy |> Data.put (Data.get lthy);
-
 
 
 (** operations **)
 
 val operations_of = #operations o get_first_lthy;