# 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);