# HG changeset patch
# User wenzelm
# Date 1564221998 -7200
# Node ID 617cd75fc3de2c1b6a237a2f88c4ba249bca2ff1
# Parent  328573dd886f8f3621a016f85a2eb62644145b44
tuned;

diff -r 328573dd886f -r 617cd75fc3de src/Pure/Proof/reconstruct.ML
--- 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