# HG changeset patch
# User wenzelm
# Date 1183658496 -7200
# Node ID d889725b0d8aff8f8b9bb966f839de50bb698da4
# Parent  e03a43b8178c88f110aebe85bf55388d7e05f8de
added is_reflexive;

diff -r e03a43b8178c -r d889725b0d8a src/Pure/more_thm.ML
--- 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;