src/Pure/context.ML

--- a/src/Pure/context.ML	Wed Jul 21 15:23:46 2010 +0200
+++ b/src/Pure/context.ML	Wed Jul 21 15:31:38 2010 +0200
@@ -41,6 +41,7 @@
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
   val get_theory: theory -> string -> theory
+  val this_theory: theory -> string -> theory
   val deref: theory_ref -> theory
   val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool
@@ -253,6 +254,10 @@
   else if #stage (history_of thy) = finished then thy
   else error ("Unfinished theory " ^ quote name);
 
+fun this_theory thy name =
+  if theory_name thy = name then thy
+  else get_theory thy name;
+
 
 (* theory references *)