# HG changeset patch
# User wenzelm
# Date 1183658490 -7200
# Node ID fd12f7d56bd7cabcc0dd8b52d94365b1436dcaee
# Parent  ba0912262b2c79b8a1636151a90e1816da3d99d2
renamed Conv.is_refl to Thm.is_reflexive;

diff -r ba0912262b2c -r fd12f7d56bd7 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Jul 05 20:01:29 2007 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Jul 05 20:01:30 2007 +0200
@@ -42,7 +42,7 @@
                    |> Drule.arg_cong_rule e
      val th' = simpex_conv (Thm.rhs_of th)
      val (l,r) = Thm.dest_equals (cprop_of th')
-    in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th))
+    in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
   | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
   | Const("All",_)$_ =>