# HG changeset patch
# User wenzelm
# Date 1208278168 -7200
# Node ID cda3df424bad31292c2aa86e088da080cc061058
# Parent  f99956db6ccde4b495b4a46236c214839da0d5dc
Facts.intern, Facts.extern_table;

diff -r f99956db6ccd -r cda3df424bad src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 15 18:49:27 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 15 18:49:28 2008 +0200
@@ -804,8 +804,7 @@
       let
         val thy = theory_of ctxt;
         val local_facts = facts_of ctxt;
-        val space = Facts.space_of local_facts;
-        val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
+        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
         val name = Facts.name_of_ref thmref;
         val thms =
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
@@ -1167,7 +1166,8 @@
   let
     val local_facts = facts_of ctxt;
     val props = Facts.props local_facts;
-    val facts = (if null props then I else cons ("unnamed", props)) (Facts.extern local_facts);
+    val facts =
+      (if null props then [] else [("unnamed", props)]) @ Facts.extern_table local_facts;
   in
     if null facts andalso not (! verbose) then []
     else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]