get_fact: report position;
authorwenzelm
Tue, 05 Aug 2008 13:31:35 +0200
changeset 27739 cd1df29db620
parent 27738 66596d7aa899
child 27740 0b22524c05e2
get_fact: report position;
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;