src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -557,7 +557,7 @@
                 (fn {context = ctxt, prems = _} =>
                   mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                     fp_nesting_pred_maps def_thms rec_thm)
-              |> Thm.close_derivation);
+              |> Thm.close_derivation \<^here>);
       in
         ((js, simps), lthy')
       end;