src/Pure/theory.ML

   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   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
   val axiom_space: theory -> Name_Space.T
   val axioms_of: theory -> (string * term) list

 fun nodes_of thy = thy :: ancestors_of thy;
 
 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 **)