# HG changeset patch
# User wenzelm
# Date 1515423011 -3600
# Node ID d5007d93bcc66a6d3b55274bd930b430cbf8e027
# Parent  c0c36348a4fb3d9593c4d2565d425b6bcba1f954
more operations;

diff -r c0c36348a4fb -r d5007d93bcc6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 08 14:59:50 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Jan 08 15:50:11 2018 +0100
@@ -8,6 +8,7 @@
 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
@@ -120,7 +121,8 @@
 
 datatype state = State of node option * node option;  (*current, previous*)
 
-fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
+fun generic_theory_toplevel gthy = State (SOME (Theory (gthy, NONE)), NONE);
+val theory_toplevel = generic_theory_toplevel o Context.Theory;
 
 val toplevel = State (NONE, NONE);