now rejects degenerate (looping) cases

--- 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 ()