# HG changeset patch # User wenzelm # Date 1515517115 -3600 # Node ID a256051dd3d6719b5c546e26bb0a4e71e5d5ad4d # Parent 7e21d19e7ad73b783994b3b4c61bf902d08e11c4 clarified presentation_state with provide presentation_context; diff -r 7e21d19e7ad7 -r a256051dd3d6 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Jan 09 17:40:25 2018 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Jan 09 17:58:35 2018 +0100 @@ -8,7 +8,6 @@ sig exception UNDEF type state - val generic_theory_toplevel: generic_theory -> state val theory_toplevel: theory -> state val toplevel: state val is_toplevel: state -> bool @@ -122,8 +121,7 @@ datatype state = State of node option * node option; (*current, previous*) -fun generic_theory_toplevel gthy = State (SOME (Theory (gthy, NONE)), NONE); -val theory_toplevel = generic_theory_toplevel o Context.Theory; +fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE); val toplevel = State (NONE, NONE); @@ -193,7 +191,7 @@ fun presentation_state ctxt = (case Presentation_State.get ctxt of - NONE => generic_theory_toplevel (Context.Proof ctxt) + NONE => State (SOME (Theory (Context.Proof ctxt, SOME ctxt)), NONE) | SOME state => state);