more compact proof terms;
authorwenzelm
Mon, 12 Aug 2019 19:47:48 +0200
changeset 70704 bf5724694ce5
parent 70703 9a9003b5c0c1
child 70705 67580f2ded90
more compact proof terms;
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
       | _ =>