src/Pure/thm.ML
changeset 50126 3dec88149176
parent 49008 a3cdb49c22cc
child 50301 56b4c9afd7be
     1.1 --- a/src/Pure/thm.ML	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/Pure/thm.ML	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4    val proof_body_of: thm -> proof_body
     1.5    val proof_of: thm -> proof
     1.6    val join_proofs: thm list -> unit
     1.7 -  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
     1.8 +  val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
     1.9    val future: thm future -> cterm -> thm
    1.10    val derivation_name: thm -> string
    1.11    val name_derivation: string -> thm -> thm
    1.12 @@ -536,12 +536,12 @@
    1.13  
    1.14  (* derivation status *)
    1.15  
    1.16 -fun status_of (Thm (Deriv {promises, body}, _)) =
    1.17 +fun peek_status (Thm (Deriv {promises, body}, _)) =
    1.18    let
    1.19      val ps = map (Future.peek o snd) promises;
    1.20      val bodies = body ::
    1.21        map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
    1.22 -    val {oracle, unfinished, failed} = Proofterm.status_of bodies;
    1.23 +    val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
    1.24    in
    1.25     {oracle = oracle,
    1.26      unfinished = unfinished orelse exists is_none ps,