same heads different arity -> INCOMPARABLE

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 024056ea221d6e2f4ec1c1f4f093716dc19655c2..1e143605b99f13127a80b72a202a56d7851bdb91 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -416,7 +416,8 @@ module LPO (B : Terms.Blob) = struct
                         if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
                       else XINCOMPARABLE
                     | o -> o)   
-                      with Invalid_argument _ -> assert false)
+                      with Invalid_argument _ -> (* assert false *)
+                              XINCOMPARABLE)
               | XINCOMPARABLE -> XINCOMPARABLE
               | _ -> assert false
           end