diff -r cd1d1bc7684c -r b9783e9e96e1 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Jul 21 13:55:44 2010 +0200
+++ b/src/Pure/context.ML	Wed Jul 21 14:27:05 2010 +0200
@@ -40,6 +40,7 @@
   val string_of_thy: theory -> string
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
+  val get_theory: theory -> string -> theory
   val deref: theory_ref -> theory
   val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool
@@ -244,6 +245,14 @@
 
 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
 
+fun get_theory thy name =
+  if theory_name thy <> name then
+    (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
+      SOME thy' => thy'
+    | NONE => error ("Unknown ancestor theory " ^ quote name))
+  else if #stage (history_of thy) = finished then thy
+  else error ("Unfinished theory " ^ quote name);
+
 
 (* theory references *)