X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=5eb3c43a5666eb9a052be298fc3cc4ed5ec0160f;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=89b390b07a11d3a9c4fc2f4f4f605c0eace95eac;hpb=ddba563cd3f42a7947a0e0b464d5dd3c5f9b299d;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 89b390b07..5eb3c43a5 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -186,12 +186,13 @@ let compare_terms o x y =
       | _ -> assert false
 ;;
 
-let are_invertible relocate alpha_eq l r =
-    let varlist = Terms.vars_of_term l in
+let are_invertible relocate alpha_eq eq_foterm l r =
+    let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) in
     let maxvar = List.fold_left max 0 varlist in
     let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
-    let l = FoSubst.apply_subst subst l in
-      try (ignore(alpha_eq l r);true) with
+    let newl = FoSubst.apply_subst subst l in
+    let newr = FoSubst.apply_subst subst r in
+      try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with
 	  FoUnif.UnificationFailure _ -> false;;
 
 module NRKBO (B : Terms.Blob) = struct
@@ -204,7 +205,7 @@ module NRKBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
 
   let compute_clause_weight = compute_clause_weight;;
   
@@ -242,7 +243,7 @@ module KBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
 
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
@@ -312,7 +313,7 @@ module LPO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
 
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;