# HG changeset patch
# User wenzelm
# Date 1518882135 -3600
# Node ID b846f7a11fda5b63b2687c6f0edc0d7ede3cfe41
# Parent  10ff1f077119edb50fd6d4afd6bb089d7e293290
clarified apply_transaction: always continue without presentation context;

diff -r 10ff1f077119 -r b846f7a11fda src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Feb 17 16:36:40 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Feb 17 16:42:15 2018 +0100
@@ -244,7 +244,7 @@
   let
     val cont_node = reset_presentation node;
     val context = cases_node I (Context.Proof o Proof.context_of) cont_node;
-    fun state_error e nd = (State (SOME nd, SOME node), e);
+    fun state_error e nd = (State (SOME nd, SOME cont_node), e);
 
     val (result, err) =
       cont_node