--- 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
| _ =>