changeset 70494 | 41108e3e9ca5 |
parent 70326 | aa7c49651f4e |
child 70507 | 06a62b29085e |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Aug 09 15:58:26 2019 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Aug 09 17:14:49 2019 +0200 @@ -384,7 +384,7 @@ #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |> Variable.export ctxt2 ctxt0 |> finish_cnf - |> map Thm.close_derivation) + |> map (Thm.close_derivation \<^here>)) end handle THM _ => (NONE, [])