# HG changeset patch
# User wenzelm
# Date 1333374170 -7200
# Node ID b0b78ce6903a9cf29879e03066cf12084d3c59c0
# Parent  2511f3e8449628040b6e3bc41acb09765b001fd5
more general Local_Theory.restore, allow any nesting level;

diff -r 2511f3e84496 -r b0b78ce6903a src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Apr 02 13:47:00 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Apr 02 15:42:50 2012 +0200
@@ -33,6 +33,7 @@
   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
@@ -54,7 +55,6 @@
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
-  val restore: local_theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
@@ -213,6 +213,8 @@
       end
   | propagate_ml_env context = context;
 
+fun restore lthy = target_of lthy |> Data.put (Data.get lthy);
+
 
 
 (** operations **)
@@ -281,10 +283,6 @@
       | _ => error "Local theory already initialized")
   |> checkpoint;
 
-fun restore lthy =
-  let val {naming, operations, target} = get_first_lthy lthy
-  in init naming operations target end;
-
 
 (* exit *)