tuned;

--- a/src/Pure/Proof/reconstruct.ML	Fri Jul 26 16:36:11 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Sat Jul 27 12:06:38 2019 +0200
@@ -330,8 +330,6 @@
 
 fun expand_proof ctxt thms prf =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     fun expand maxidx prfs (AbsP (s, t, prf)) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', AbsP (s, t, prf')) end