X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=f7062b3abebbe2b4d95956ec6f024fd4b46dcb07;hb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;hp=1e143605b99f13127a80b72a202a56d7851bdb91;hpb=2e7aca462b7556a3a7369de030bbac8d8205aa92;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 1e143605b..f7062b3ab 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -40,7 +40,8 @@ let rec eq_foterm f x y =
     match x, y with
     | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
     | Terms.Var i, Terms.Var j -> i = j
-    | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
+    | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 -> 
+        List.for_all2 (eq_foterm f) l1 l2
     | _ -> false
 ;;