1.1 --- a/src/Pure/global_theory.ML	Sun Mar 18 13:37:11 2012 +0100
     1.2 +++ b/src/Pure/global_theory.ML	Sun Mar 18 13:51:51 2012 +0100
     1.3 @@ -91,8 +91,6 @@
     1.4  
     1.5  fun get_fact context thy xthmref =
     1.6    let
     1.7 -    val ctxt = Context.proof_of context;
     1.8 -
     1.9      val facts = facts_of thy;
    1.10      val xname = Facts.name_of_ref xthmref;
    1.11      val pos = Facts.pos_of_ref xthmref;
    1.12 @@ -107,9 +105,9 @@
    1.13      (case res of
    1.14        NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
    1.15      | SOME (static, ths) =>
    1.16 -        (Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name);
    1.17 +        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
    1.18           if static then ()
    1.19 -         else Context_Position.report ctxt pos (Isabelle_Markup.dynamic_fact name);
    1.20 +         else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
    1.21           Facts.select xthmref (map (Thm.transfer thy) ths)))
    1.22    end;
    1.23