# HG changeset patch
# User wenzelm
# Date 1515519021 -3600
# Node ID 1256460c063a867ff486e5a0e21899aae7930082
# Parent  d55e52e25d9ab79d264b6840889c977e4c272f55
tuned;

diff -r d55e52e25d9a -r 1256460c063a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:18:21 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:30:21 2018 +0100
@@ -114,8 +114,6 @@
   | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
   | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
 
-val context_node = cases_node Context.proof_of Proof.context_of;
-
 
 (* datatype state *)
 
@@ -183,7 +181,7 @@
 fun presentation_context state =
   (case try node_of state of
     SOME (Theory (_, SOME ctxt)) => ctxt
-  | SOME node => context_node node
+  | SOME node => cases_node Context.proof_of Proof.context_of node
   | NONE =>
       (case try Theory.get_pure () of
         SOME thy => Proof_Context.init_global thy