src/HOL/Tools/Meson/meson_clausify.ML
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, [])