src/Pure/Isar/theory_target.ML

     val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = PureThy.name_thm true (name, Goal.close_result th'');
+    val result = th''
+      |> PureThy.name_thm true true ""
+      |> Goal.close_result
+      |> PureThy.name_thm true true name;
 
     (*import fixes*)
     val (tvars, vars) =
       chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
       |>> map Logic.dest_type;

     val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms);
     val result'' =
       (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
         NONE => raise THM ("Failed to re-import result", 0, [result'])
       | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2)
-      |> Goal.norm_result;
+      |> Goal.norm_result
+      |> PureThy.name_thm false false name;
 
   in (result'', result) end;
 
 fun notes loc kind facts lthy =
   let