src/Pure/thm.ML
changeset 30711 952fdbee1b48
parent 30556 7be15917f3fa
child 30713 b1a87e3971a3
     1.1 --- a/src/Pure/thm.ML	Tue Mar 24 19:37:50 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Mar 24 21:24:53 2009 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val theory_of_thm: thm -> theory
     1.5    val prop_of: thm -> term
     1.6    val tpairs_of: thm -> (term * term) list
     1.7 +  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
     1.8    val concl_of: thm -> term
     1.9    val prems_of: thm -> term list
    1.10    val nprems_of: thm -> int
    1.11 @@ -399,6 +400,7 @@
    1.12  val hyps_of = #hyps o rep_thm;
    1.13  val prop_of = #prop o rep_thm;
    1.14  val tpairs_of = #tpairs o rep_thm;
    1.15 +fun status_of (Thm (Deriv {body, ...}, _)) = Pt.status_of body;
    1.16  
    1.17  val concl_of = Logic.strip_imp_concl o prop_of;
    1.18  val prems_of = Logic.strip_imp_prems o prop_of;