# HG changeset patch
# User wenzelm
# Date 1217935895 -7200
# Node ID cd1df29db6206624df270b6f83ce3967e8eb2d71
# Parent  66596d7aa899dc27e4f61f99c24ceecd9ff1f75a
get_fact: report position;

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;