src/Pure/theory.ML
changeset 70067 0cb8753bdb50
parent 69295 bf6937af7fe8
     1.1 --- a/src/Pure/theory.ML	Sat Mar 09 13:35:49 2019 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Mar 09 23:57:07 2019 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val local_setup: (Proof.context -> Proof.context) -> unit
     1.5    val install_pure: theory -> unit
     1.6    val get_pure: unit -> theory
     1.7 +  val get_pure_bootstrap: unit -> theory
     1.8    val get_markup: theory -> Markup.T
     1.9    val check: {long: bool} -> Proof.context -> string * Position.T -> theory
    1.10    val axiom_table: theory -> term Name_Space.table
    1.11 @@ -59,6 +60,11 @@
    1.12      SOME thy => thy
    1.13    | NONE => raise Fail "Theory Pure not present");
    1.14  
    1.15 +fun get_pure_bootstrap () =
    1.16 +  (case Single_Assignment.peek pure of
    1.17 +    SOME thy => thy
    1.18 +  | NONE => Context.the_global_context ());
    1.19 +
    1.20  
    1.21  
    1.22  (** datatype thy **)