added is_reflexive;

--- a/src/Pure/more_thm.ML	Thu Jul 05 20:01:35 2007 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 05 20:01:36 2007 +0200
@@ -21,6 +21,7 @@
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
   val thm_ord: thm * thm -> order
+  val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
   val eq_thm_thy: thm * thm -> bool
@@ -114,6 +115,9 @@
 
 (* equality *)
 
+fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
+  handle TERM _ => false;
+
 fun eq_thm ths =
   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   thm_ord ths = EQUAL;