# 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