diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -275,7 +275,7 @@
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
       |> fold_rev Thm.forall_intr cqs
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
   in
     replace_lemma
   end
@@ -426,7 +426,7 @@
             (Term.add_vars (Thm.prop_of it) []) it)
 
     val goalstate =  Conjunction.intr graph_is_function complete
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
       |> Thm.implies_intr (Thm.cprop_of complete)