tuned;

--- a/src/Pure/global_theory.ML	Sun Mar 18 13:37:11 2012 +0100
+++ b/src/Pure/global_theory.ML	Sun Mar 18 13:51:51 2012 +0100
@@ -91,8 +91,6 @@
 
 fun get_fact context thy xthmref =
   let
-    val ctxt = Context.proof_of context;
-
     val facts = facts_of thy;
     val xname = Facts.name_of_ref xthmref;
     val pos = Facts.pos_of_ref xthmref;
@@ -107,9 +105,9 @@
     (case res of
       NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
     | SOME (static, ths) =>
-        (Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name);
+        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
          if static then ()
-         else Context_Position.report ctxt pos (Isabelle_Markup.dynamic_fact name);
+         else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
          Facts.select xthmref (map (Thm.transfer thy) ths)))
   end;