--- a/src/Pure/goal.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/goal.ML Fri Aug 09 17:14:49 2019 +0200
@@ -136,7 +136,7 @@
Thm.solve_constraints);
val local_result =
Thm.future global_result global_prop
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Thm.instantiate (instT, [])
|> Drule.forall_elim_list fixes
|> fold (Thm.elim_implies o Thm.assume) assms
@@ -220,7 +220,7 @@
(Thm.term_of stmt);
in
res
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length props)
|> map (Assumption.export false ctxt' ctxt)
|> Variable.export ctxt' ctxt