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