X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=d6454f2027d4799fdf2dd49bf1ade2bdd685f24d;hb=249d79bebff886846fbab65cc079623d90684baf;hp=42703045d0019616b041af03fd1031d02ab66f4f;hpb=2daf59a983cae8151e513196577ae77b1d12e157;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 42703045d..d6454f202 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -84,8 +84,15 @@ let weight_of_term ?(consider_metas=true) term =
 
 
 let compute_equality_weight ty left right =
-  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
-  (weight_of ty) + (weight_of left) + (weight_of right)
+  let metasw = ref 0 in
+  let weight_of t =
+    let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
+(*     let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
+(*     metasw := !metasw + mw; *)
+    metasw := !metasw + (2 * (List.length m));
+    w
+  in
+  (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
 ;;