src/HOL/Library/EfficientNat.thy

--- a/src/HOL/Library/EfficientNat.thy	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu May 11 19:19:31 2006 +0200
@@ -208,7 +208,7 @@
             (Thm.forall_intr (cert v) th'))
         in
           remove_suc_clause thy (map (fn th''' =>
-            if th''' = th then th'' else th''') thms)
+            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
         end
   end;