# HG changeset patch
# User wenzelm
# Date 1332075111 -3600
# Node ID 0dacedb4a94820982e1b14ee1530862d664151ff
# Parent  5ee8004e215119e082ab99234fba64578dd10bf8
tuned;

diff -r 5ee8004e2151 -r 0dacedb4a948 src/Pure/global_theory.ML
--- 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;