avoid arcane Local_Theory.reinit entirely

--- 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 *)