--- a/src/Pure/proofterm.ML Sat Jul 18 22:52:31 2009 +0200
+++ b/src/Pure/proofterm.ML Sat Jul 18 22:53:02 2009 +0200
@@ -43,6 +43,7 @@
val proof_of: proof_body -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+ val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -185,6 +186,8 @@
in (f (name, prop, body') x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
+
fun status_of bodies =
let
fun status (PBody {oracles, thms, ...}) x =