--- 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)