changeset 70494 | 41108e3e9ca5 |
parent 70473 | 9179e7a98196 |
child 72154 | 2b41b710f6ef |
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Aug 09 15:58:26 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Aug 09 17:14:49 2019 +0200 @@ -664,7 +664,7 @@ let val rsp_thm = Goal.prove_sorry lthy [] [] goal (tac o #context) - |> Thm.close_derivation + |> Thm.close_derivation \<^here> in after_qed rsp_thm lthy end