tuned;
authorwenzelm
Tue Jan 09 18:30:21 2018 +0100 (17 months ago ago)
changeset 673921256460c063a
parent 67391 d55e52e25d9a
child 67393 be88c2bc8a45
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:18:21 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:30:21 2018 +0100
     1.3 @@ -114,8 +114,6 @@
     1.4    | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
     1.5    | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
     1.6  
     1.7 -val context_node = cases_node Context.proof_of Proof.context_of;
     1.8 -
     1.9  
    1.10  (* datatype state *)
    1.11  
    1.12 @@ -183,7 +181,7 @@
    1.13  fun presentation_context state =
    1.14    (case try node_of state of
    1.15      SOME (Theory (_, SOME ctxt)) => ctxt
    1.16 -  | SOME node => context_node node
    1.17 +  | SOME node => cases_node Context.proof_of Proof.context_of node
    1.18    | NONE =>
    1.19        (case try Theory.get_pure () of
    1.20          SOME thy => Proof_Context.init_global thy