Facts.add_global;

--- a/src/Pure/pure_thy.ML	Mon Mar 17 20:51:09 2008 +0100
+++ b/src/Pure/pure_thy.ML	Mon Mar 17 20:51:16 2008 +0100
@@ -353,7 +353,7 @@
         val r as ref (Thms {theorems = (space, theorems), all_facts}) = get_theorems_ref thy';
         val space' = Sign.declare_name thy' name space;
         val theorems' = Symtab.update (name, thms') theorems;
-        val all_facts' = Facts.add false (Sign.naming_of thy') (name, thms') all_facts;
+        val all_facts' = Facts.add_global (Sign.naming_of thy') (name, thms') all_facts;
       in
         (case Symtab.lookup theorems name of
           NONE => ()