# 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