From: denes <??>
Date: Wed, 22 Jul 2009 15:43:57 +0000 (+0000)
Subject: Fixed test for invertibility
X-Git-Tag: make_still_working~3631
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87f1e71f269122c42c02971c82406767e3395ca5;p=helm.git

Fixed test for invertibility
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 4c6e0a977..7743e3726 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -249,12 +249,14 @@ let relocate maxvar varlist subst =
   ;;
 
   let are_invertible l r =
-    let varlist = Terms.vars_of_term l in
+    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
 	  UnificationFailure _ -> false
+;;
 
   let compute_unit_clause_weight = compute_unit_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;