tuned;
authorwenzelm
Sat, 27 Jul 2019 12:06:38 +0200
changeset 70606 617cd75fc3de
parent 70605 328573dd886f
child 70607 d6a5301f9ffb
tuned;
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