# HG changeset patch
# User wenzelm
# Date 1515503259 -3600
# Node ID e32b0eb63666f4cddd1e6685ca180f192f1953a6
# Parent  aacea75450b4b4968050244c8e540aad3b9c98cb
clarified exception;

diff -r aacea75450b4 -r e32b0eb63666 src/Pure/theory.ML
--- 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 **)