X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=51b48a4c32951f4fc7c9cc9ea2a9ca18a0df5ab9;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=8f0575a674aeffdd3ea153a1e859b7cb8a603c79;hpb=9ab150d29e4b7653f71085da477a1c81f7b7e131;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 8f0575a67..51b48a4c3 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -49,12 +49,12 @@ module Orderings (B : Terms.Blob) = struct
     (w, List.sort compare l) (* from the smallest meta to the bigest *)
   ;;
   
-  let compute_unit_clause_weight = 
+  let compute_unit_clause_weight (_,l, _, _) = 
     let weight_of_polynomial w m =
       let factor = 2 in      
       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
     in
-    function
+    match l with
     | Terms.Predicate t -> 
         let w, m = weight_of_term t in 
         weight_of_polynomial w m