# HG changeset patch
# User wenzelm
# Date 1333378832 -7200
# Node ID ea089b484157d52298d6593db98fcbac77aa77c0
# Parent  ca31cfa509b1ece72c1fc209eaf70e846266b2c2
better restore to first target, not last target;

diff -r ca31cfa509b1 -r ea089b484157 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Apr 02 16:35:09 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Apr 02 17:00:32 2012 +0200
@@ -11,6 +11,7 @@
 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
@@ -33,7 +34,6 @@
   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
@@ -107,6 +107,8 @@
   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 *)
 
@@ -213,8 +215,6 @@
       end
   | propagate_ml_env context = context;
 
-fun restore lthy = target_of lthy |> Data.put (Data.get lthy);
-
 
 
 (** operations **)