added the_theory;

--- a/src/Pure/Thy/thy_info.ML	Tue May 02 20:42:42 2006 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue May 02 20:42:43 2006 +0200
@@ -32,6 +32,7 @@
   val if_known_thy: (string -> unit) -> string -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
+  val the_theory: string -> theory -> theory
   val get_preds: string -> string list
   val loaded_files: string -> Path.T list
   val touch_child_thys: string -> unit
@@ -195,6 +196,10 @@
     (SOME theory) => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
+fun the_theory name thy =
+  if Context.theory_name thy = name then thy
+  else get_theory name;
+
 fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));