# HG changeset patch
# User wenzelm
# Date 1247950382 -7200
# Node ID db50e76b0046374c050f005522514e19f0e134d1
# Parent  257eac3946e992560c74942324e1510ce2b78788
added join_bodies;

diff -r 257eac3946e9 -r db50e76b0046 src/Pure/proofterm.ML
--- 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 =