src/Pure/Isar/isar_syn.ML

   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
     (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
 
 val endP =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
-    (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.exit_local_theory));
+    (Scan.succeed (Toplevel.exit o Toplevel.exit_local_theory));
 
 val contextP =
   OuterSyntax.improper_command "context" "switch (local) theory context"
     (K.tag_theory K.thy_switch)
-    (P.name >> (Toplevel.print oo IsarThy.context));
-
+    (P.name --| P.begin >> (fn name =>
+      Toplevel.print o IsarThy.context name o
+      Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
 
 
 (** markup commands **)
 
 val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag

   OuterSyntax.command "locale" "define named proof context" K.thy_decl
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
         -- P.opt_begin
       >> (fn (((is_open, name), (expr, elems)), begin) =>
-          Toplevel.begin_local_theory begin (Locale.add_locale is_open name expr elems)));
+          Toplevel.begin_local_theory begin
+            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
 
 val interpretationP =
   OuterSyntax.command "interpretation"
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr

     (Scan.succeed (Toplevel.print o IsarCmd.back));
 
 
 (* history *)
 
-val cannot_undoP =    (* FIXME ProofGeneral compatibility *)
-  OuterSyntax.improper_command "cannot_undo" "attempt to undo 'end'" K.control
-    (P.name >> K (Toplevel.no_timing o IsarCmd.undo_end));
-
-val undo_endP =
-  OuterSyntax.improper_command "undo_end" "attempt to undo 'end'" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo_end));
+val cannot_undoP =
+  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
+    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
 
 val clear_undosP =
   OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
     (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory));
 

   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
   qedP, terminal_proofP, default_proofP, immediate_proofP,
   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
-  cannot_undoP, undo_endP, clear_undosP, redoP, undos_proofP, undoP,
-  killP, interpretationP, interpretP,
+  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
+  interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,