--- 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;