# HG changeset patch
# User wenzelm
# Date 1565632068 -7200
# Node ID bf5724694ce5248610f01bcb44b3b6880ded0736
# Parent  9a9003b5c0c164555cfcf626ee50e1a41f4560b3
more compact proof terms;

diff -r 9a9003b5c0c1 -r bf5724694ce5 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 19:29:33 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 19:47:48 2019 +0200
@@ -185,7 +185,7 @@
     val th1' = incr_type_indexes ctxt (Thm.maxidx_of th2 + 1) th1
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
-            (false, tha, Thm.nprems_of tha) i thb
+            (false, Thm.close_derivation \<^here> tha, Thm.nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
         [th] => th
       | _ =>