--- a/src/Pure/thm.ML Tue Mar 24 19:37:50 2009 +0100
+++ b/src/Pure/thm.ML Tue Mar 24 21:24:53 2009 +0100
@@ -60,6 +60,7 @@
val theory_of_thm: thm -> theory
val prop_of: thm -> term
val tpairs_of: thm -> (term * term) list
+ val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val concl_of: thm -> term
val prems_of: thm -> term list
val nprems_of: thm -> int
@@ -399,6 +400,7 @@
val hyps_of = #hyps o rep_thm;
val prop_of = #prop o rep_thm;
val tpairs_of = #tpairs o rep_thm;
+fun status_of (Thm (Deriv {body, ...}, _)) = Pt.status_of body;
val concl_of = Logic.strip_imp_concl o prop_of;
val prems_of = Logic.strip_imp_prems o prop_of;