--- a/src/Pure/theory.ML Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/theory.ML Mon Jan 08 22:36:02 2018 +0100
@@ -11,6 +11,8 @@
val nodes_of: theory -> theory list
val setup: (theory -> theory) -> unit
val local_setup: (Proof.context -> Proof.context) -> unit
+ val get_pure: unit -> theory
+ val install_pure: theory -> unit
val get_markup: theory -> Markup.T
val check: Proof.context -> string * Position.T -> theory
val axiom_table: theory -> term Name_Space.table
@@ -45,6 +47,10 @@
fun setup f = Context.>> (Context.map_theory f);
fun local_setup f = Context.>> (Context.map_proof f);
+val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
+fun get_pure () = the (Single_Assignment.peek pure);
+fun install_pure thy = Single_Assignment.assign pure thy;
+
(** datatype thy **)