# HG changeset patch
# User wenzelm
# Date 1445609346 -7200
# Node ID 6865140215ef9508a34971869fe165bc4d8cab27
# Parent  436b7fe89cdc748d3bbff32475834a961ae1a810
proper transfer of stored facts;

diff -r 436b7fe89cdc -r 6865140215ef src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Oct 22 23:01:49 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Fri Oct 23 16:09:06 2015 +0200
@@ -58,19 +58,23 @@
 
 fun unused_thms (base_thys, thys) =
   let
-    fun add_fact space (name, ths) =
+    fun add_fact transfer space (name, ths) =
       if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
       else
         let val {concealed, group, ...} = Name_Space.the_entry space name in
           fold_rev (fn th =>
             (case Thm.derivation_name th of
               "" => I
-            | a => cons (a, (th, concealed, group)))) ths
+            | a => cons (a, (transfer th, concealed, group)))) ths
         end;
-    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
+    fun add_facts thy =
+      let
+        val transfer = Global_Theory.transfer_theories thy;
+        val facts = Global_Theory.facts_of thy;
+      in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;
 
     val new_thms =
-      fold (add_facts o Global_Theory.facts_of) thys []
+      fold add_facts thys []
       |> sort_distinct (string_ord o apply2 #1);
 
     val used =