src/Pure/Tools/debugger.ML

         (case Document.command_exec (Document.state ()) node_name id of
           SOME (eval, _) =>
             if Command.eval_finished eval then
               let
                 val st = Command.eval_result_state eval;
-                val ctxt = Toplevel.presentation_context st
-                  handle Toplevel.UNDEF => err ();
+                val ctxt = Toplevel.presentation_context st;
               in
                 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
                   SOME (b, _) => b := breakpoint_state
                 | NONE => err ())
               end