diff -r 766e7f50c22f -r 56f3351cc492 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -115,8 +115,8 @@
   | named_begin NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.restore, lthy)
   | named_begin (SOME loc) (Context.Proof lthy) =
-      (Context.Proof o Named_Target.reinit lthy,
-        named_init loc (named_exit (Local_Theory.assert_nonbrittle lthy)));
+      (Context.Proof o Named_Target.init (the (Named_Target.locale_of lthy)) o named_exit,
+        (named_init loc o named_exit o Local_Theory.assert_nonbrittle) lthy);
 
 
 (* datatype node *)