# HG changeset patch
# User paulson
# Date 1094481910 -7200
# Node ID 66da80cad4a2ea966f67cc08985ab6901d3ba9de
# Parent  5cea84e10f3efa01cef9666b5cddcdcc58508da1
now rejects degenerate (looping) cases

diff -r 5cea84e10f3e -r 66da80cad4a2 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Mon Sep 06 15:57:58 2004 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Mon Sep 06 16:45:10 2004 +0200
@@ -166,6 +166,8 @@
        and rt' = cancelled rtms
 
        val rhs = rel$lt'$rt'
+       val _ = if lhs aconv rhs then raise Cancel  (*nothing to do*)
+                                     else ()
        val _ = if !trace then
                  tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
                else ()