# HG changeset patch
# User wenzelm
# Date 1519047006 -3600
# Node ID 3f330245aebe33e514ae25eb3dea165c12c15b55
# Parent  50db601cba270136094b1f8a7351ffb5973b726b
tuned: more accurate transfer;

diff -r 50db601cba27 -r 3f330245aebe src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Feb 19 14:26:37 2018 +0100
+++ b/src/Pure/global_theory.ML	Mon Feb 19 14:30:06 2018 +0100
@@ -133,11 +133,10 @@
     let
       val name = Sign.full_name thy b;
       val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
-      val thms'' = map (Thm.transfer thy') thms';
       val thy'' = thy' |> Data.map
         (Facts.add_static (Context.Theory thy') {strict = true, index = false}
-          (b, Lazy.value thms'') #> snd);
-    in (thms'', thy'') end;
+          (b, Lazy.value thms') #> snd);
+    in (map (Thm.transfer thy'') thms', thy'') end;
 
 
 (* store_thm(s) *)