--- a/src/Pure/theory.ML Tue Jan 09 00:17:12 2018 +0100
+++ b/src/Pure/theory.ML Tue Jan 09 14:07:39 2018 +0100
@@ -11,8 +11,8 @@
val nodes_of: theory -> theory list
val setup: (theory -> theory) -> unit
val local_setup: (Proof.context -> Proof.context) -> unit
+ val install_pure: theory -> 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
@@ -47,10 +47,18 @@
fun setup f = Context.>> (Context.map_theory f);
fun local_setup f = Context.>> (Context.map_proof f);
+
+(* implicit theory Pure *)
+
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;
+fun get_pure () =
+ (case Single_Assignment.peek pure of
+ SOME thy => thy
+ | NONE => raise Fail "Theory Pure not present");
+
(** datatype thy **)