# HG changeset patch
# User wenzelm
# Date 1564417011 -7200
# Node ID 03cfef16ddb4551080f8d546fa65a7a92cbb177d
# Parent  145fb19d906d29464f2559ce69c681fe9adcfb96
more diagnostic operations;

diff -r 145fb19d906d -r 03cfef16ddb4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 15:10:30 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 18:16:51 2019 +0200
@@ -54,8 +54,9 @@
   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
-  val no_proof_body: proof_body
+  val no_proof_body: proof -> proof_body
   val no_thm_proofs: proof -> proof
+  val no_body_proofs: proof -> proof
 
   val encode: proof XML.Encode.T
   val encode_body: proof_body XML.Encode.T
@@ -310,8 +311,8 @@
       proof = prf}
   end;
 
-val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof};
-val no_body = Future.value no_proof_body;
+fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
+val no_body = Future.value (no_proof_body MinProof);
 
 fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body))
   | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -320,6 +321,14 @@
   | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2
   | no_thm_proofs a = a;
 
+fun no_body_proofs (PThm (i, (a, body))) =
+      PThm (i, (a, Future.value (no_proof_body (join_proof body))))
+  | no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf)
+  | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
+  | no_body_proofs (prf % t) = no_body_proofs prf % t
+  | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
+  | no_body_proofs a = a;
+
 
 
 (** XML data representation **)