src/HOL/Tools/BNF/bnf_fp_util.ML

 
     val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
       (map2 (flip mk_leq) relphis pre_phis));
   in
     Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
 fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
   let

 
     val goal = fold_rev Logic.all (phis @ pre_ophis)
       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   in
     Goal.prove_sorry lthy [] [] goal tac
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> split_conj_thm
   end;
 
 fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
     map_cong0s =

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
             xtor_un_fold_unique xtor_un_folds map_comps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> split_conj_thm
       end;
 
     val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs;
     val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss;

         map2 (fn goal => fn un_fold =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} =>
               mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals xtor_un_folds
       end;
 
     val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs;
     val co_rec_expand'_thms = map (fn thm =>

         val inverses = maps mk_inverses absT_info_opts;
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
             co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s inverses)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts
       then
         mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm