src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

             (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
               mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                 def_thms rec_thm
               |> K |> Goal.prove_sorry lthy' [] [] user_eqn
-              |> singleton (Proof_Context.export lthy' lthy)
-              (* for code extraction from proof terms: *)
-              |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^
-                Long_Name.separator ^ simpsN ^
-                (if js = [0] then "" else "_" ^ string_of_int (j + 1))))
+              |> Thm.close_derivation)
             js;
       in
         (js, simp_thms)
       end;