the old compute_eq_weight is back (no more max)

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index a25ba8e2d7cda49cb9ac8cfede5cb14ea2aef99d..542c2dd77d26e6c6bae42937abd63d9fc2257a72 100644 (file)
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -318,7 +318,7 @@ let compute_equality_weight (ty,left,right,o) =
               ~consider_metas:true ~count_metas_occurrences:false right) in
       let w2, m2 = (weight_of_term 
               ~consider_metas:true ~count_metas_occurrences:false left) in
-      (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2)))
+      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
 ;;
 
 (* old