# HG changeset patch
# User wenzelm
# Date 1566306726 -7200
# Node ID 78426ea26f125e4d03c330557e3036f666b13929
# Parent  38cc9b2c5a94f34a4d4243ae27d632296a0b484c
unused (see 095dadc62bb5);

diff -r 38cc9b2c5a94 -r 78426ea26f12 src/Pure/thm.ML
--- 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 [] = ()