# HG changeset patch
# User wenzelm
# Date 1205783476 -3600
# Node ID 73d68876ba46fb8b456df680492df3646f52f6a1
# Parent  27d3de85c26603298f27bd4f9c82f51bc1104eaa
Facts.add_global;

diff -r 27d3de85c266 -r 73d68876ba46 src/Pure/pure_thy.ML
--- 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 => ()