tuned: more accurate transfer;

--- 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) *)