src/Pure/Thy/thy_info.ML
changeset 60937 51425cbe8ce9
parent 59366 e94df7f6b608
child 60975 5f3d6e16ea78
--- a/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -10,6 +10,7 @@
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
+  val pure_theory: unit -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
@@ -100,6 +101,8 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
+fun pure_theory () = get_theory "Pure";
+
 val get_imports = Resources.imports_of o get_theory;