--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Aug 12 15:44:41 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Aug 12 17:15:41 2019 +0200
@@ -176,7 +176,8 @@
| get_isa_thm mth Isa_Lambda_Lifted =
lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm _ (Isa_Raw ith) = ith
- val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
+ val axioms = axioms |> map (fn (mth, ith) =>
+ (mth, get_isa_thm mth ith |> Thm.close_derivation \<^here>))
val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
val _ = trace_msg ctxt (K "METIS CLAUSES")