src/HOL/Tools/BNF/bnf_lfp_compat.ML

       unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN
       HEADGOAL (rtac ctxt refl);
 
     fun prove goal =
       Goal.prove_sorry ctxt [] [] goal (tac o #context)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
   in
     map (map prove) goalss
   end;
 
 fun define_split_rec_derive_induct_rec_thms Xs fpTs ctrXs_Tsss ctrss inducts induct recs0 rec_thmss