# HG changeset patch
# User wenzelm
# Date 1237931749 -3600
# Node ID fc9d8b1bf1e0ead8b1e4bbc4590652d58c225167
# Parent  952fdbee1b48424cb7dc900d975479094e444cbd
status_of: simultaneous list;

diff -r 952fdbee1b48 -r fc9d8b1bf1e0 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Mar 24 21:24:53 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Mar 24 22:55:49 2009 +0100
@@ -42,7 +42,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 status_of: proof_body -> {failed: bool, oracle: bool, unfinished: bool}
+  val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
@@ -186,7 +186,7 @@
         in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
-fun status_of proof_body =
+fun status_of bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
       let
@@ -205,7 +205,7 @@
                     in ((oracle, true, failed), seen') end)
               end);
       in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
-    val (oracle, unfinished, failed) = #1 (status proof_body ((false, false, false), Inttab.empty));
+    val (oracle, unfinished, failed) = #1 (fold status bodies ((false, false, false), Inttab.empty));
   in {oracle = oracle, unfinished = unfinished, failed = failed} end;