--- a/src/Pure/Isar/toplevel.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 12 13:28:18 2010 +0200
@@ -112,8 +112,7 @@
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' => let
- val target_name = #target (Named_Target.peek lthy);
- val target = if target_name = "" then NONE else SOME target_name;
+ val target = #target (Named_Target.peek lthy);
in Context.Proof (Named_Target.init target (loc_exit lthy')) end;