--- a/src/Pure/thm.ML Tue Aug 20 15:07:36 2019 +0200 +++ b/src/Pure/thm.ML Tue Aug 20 15:12:06 2019 +0200 @@ -736,7 +736,6 @@ (* fulfilled proofs *) -fun raw_body_of (Thm (Deriv {body, ...}, _)) = body; fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; fun join_promises [] = ()