Facts.extern_static;

--- a/src/Pure/Isar/proof_context.ML	Wed Apr 16 21:53:02 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 16 21:53:03 2008 +0200
@@ -1156,7 +1156,7 @@
     val local_facts = facts_of ctxt;
     val props = Facts.props local_facts;
     val facts =
-      (if null props then [] else [("unnamed", props)]) @ Facts.extern_table local_facts;
+      (if null props then [] else [("unnamed", props)]) @ Facts.extern_static local_facts;
   in
     if null facts andalso not (! verbose) then []
     else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]