more compact proof terms;
authorwenzelm
Mon, 12 Aug 2019 17:15:41 +0200
changeset 70700 7a63b16c53c4
parent 70699 dc749e0dc6b2
child 70701 c04e2426f319
more compact proof terms;
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")