diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/theory.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -16,6 +16,7 @@
   val setup: (theory -> theory) -> unit
   val local_setup: (Proof.context -> Proof.context) -> unit
   val get_markup: theory -> Markup.T
+  val check: Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
   val axioms_of: theory -> (string * term) list
@@ -128,6 +129,25 @@
   let val {pos, id, ...} = rep_theory thy
   in theory_markup false (Context.theory_name thy) id pos end;
 
+fun check ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val thy' =
+      Context.get_theory thy name
+        handle ERROR msg =>
+          let
+            val completion =
+              Completion.make (name, pos)
+                (fn completed =>
+                  map Context.theory_name (ancestors_of thy)
+                  |> filter completed
+                  |> sort_strings
+                  |> map (fn a => (a, (Markup.theoryN, a))));
+            val report = Markup.markup_report (Completion.reported_text completion);
+          in error (msg ^ Position.here pos ^ report) end;
+    val _ = Context_Position.report ctxt pos (get_markup thy');
+  in thy' end;
+
 
 (* basic operations *)