# HG changeset patch
# User wenzelm
# Date 1565622941 -7200
# Node ID 7a63b16c53c44109c2c329429d8b6bcc6ecc3f21
# Parent  dc749e0dc6b290bd52a1e98cdf75c6d7a63b9ab9
more compact proof terms;

diff -r dc749e0dc6b2 -r 7a63b16c53c4 src/HOL/Tools/Metis/metis_tactic.ML
--- 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")