# HG changeset patch
# User wenzelm
# Date 1208375583 -7200
# Node ID 65106c87b688f64f3a459d4d43aec6324762500a
# Parent  29f5c1a296bc55f7f094d6db40a3883a5be5731a
Facts.extern_static;

diff -r 29f5c1a296bc -r 65106c87b688 src/Pure/Isar/proof_context.ML
--- 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)]