diff -r 66596d7aa899 -r cd1df29db620 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Aug 05 13:31:31 2008 +0200 +++ b/src/Pure/pure_thy.ML Tue Aug 05 13:31:35 2008 +0200 @@ -150,7 +150,9 @@ in (case res of NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) - | SOME ths => Facts.select xthmref (map (Thm.transfer thy) ths)) + | SOME (static, ths) => + (Position.report ((if static then Markup.fact else Markup.dynamic_fact) name) pos; + Facts.select xthmref (map (Thm.transfer thy) ths))) end; fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;