diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -567,7 +567,7 @@
       (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;
 
@@ -586,7 +586,7 @@
       (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;
 
@@ -796,7 +796,7 @@
         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;
 
@@ -825,7 +825,7 @@
           |> (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;
 
@@ -856,7 +856,7 @@
         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