changeset 70494 | 41108e3e9ca5 |
parent 70398 | 725438ceae7c |
child 70520 | 11d8517d9384 |
--- a/src/Pure/Isar/proof.ML Fri Aug 09 15:58:26 2019 +0200 +++ b/src/Pure/Isar/proof.ML Fri Aug 09 17:14:49 2019 +0200 @@ -497,7 +497,7 @@ fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal); val th = - (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ()) + (Goal.conclude (Thm.close_derivation \<^here> goal) handle THM _ => err_lost ()) |> Drule.flexflex_unique (SOME ctxt) |> Thm.check_shyps ctxt |> Thm.check_hyps (Context.Proof ctxt);