1.1 --- a/src/Pure/thm.ML	Sat Jan 10 16:53:12 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Jan 10 16:54:55 2009 +0100
     1.3 @@ -146,6 +146,7 @@
     1.4    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     1.5    val freezeT: thm -> thm
     1.6    val future: thm future -> cterm -> thm
     1.7 +  val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
     1.8    val proof_body_of: thm -> proof_body
     1.9    val proof_of: thm -> proof
    1.10    val join_proof: thm -> unit
    1.11 @@ -1626,7 +1627,13 @@
    1.12    end;
    1.13  
    1.14  
    1.15 -(* fulfilled proof *)
    1.16 +(* pending task groups *)
    1.17 +
    1.18 +fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
    1.19 +  fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
    1.20 +
    1.21 +
    1.22 +(* fulfilled proofs *)
    1.23  
    1.24  fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
    1.25