src/Pure/Isar/toplevel.ML
changeset 38389 d7d915bae307
parent 38388 94d5624dd1f7
child 38391 ba1cc1815ce1
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:23:46 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:28:18 2010 +0200
     1.3 @@ -112,8 +112,7 @@
     1.4  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
     1.5    | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
     1.6    | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
     1.7 -        val target_name = #target (Named_Target.peek lthy);
     1.8 -        val target = if target_name = "" then NONE else SOME target_name;
     1.9 +        val target = #target (Named_Target.peek lthy);
    1.10        in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
    1.11  
    1.12