# HG changeset patch
# User haftmann
# Date 1281539762 -7200
# Node ID cf42d8355844719b3ab476f35dc6e845b2402387
# Parent  67d71449e85ba993e8a3bece93f676417b4e9d3b
avoid arcane Local_Theory.reinit entirely

diff -r 67d71449e85b -r cf42d8355844 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 16:02:03 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 17:16:02 2010 +0200
@@ -112,8 +112,10 @@
 
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
-  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
-      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
+  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
+        val target_name = #target (Named_Target.peek lthy);
+        val target = if target_name = "" then NONE else SOME target_name;
+      in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
 
 
 (* datatype node *)