X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=05fdbe37cdca5b4b301a0e840890cc5337cf173a;hb=9883f04161a9972f0641dd85faf224b4f2846f05;hp=3a5c241f515394273795a6fdc62d83b6b3200fa8;hpb=a6011d00d7c377056ead2e0974c68a7a3ae069d0;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 3a5c241f5..05fdbe37c 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -78,31 +78,30 @@ module Founif (B : Terms.Blob) = struct
           raise (UnificationFailure (lazy "Inference.unification.unif"))
     in
     let subst = unif Subst.id_subst t1 t2 in
-    let vars = Subst.filter subst vars in
-    subst, vars
+    subst
 ;;
 
   let alpha_eq s t =
     let rec equiv subst s t =
       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
-	
+        
       in
       match s, t with
-	| s, t when U.eq_foterm s t -> subst
-	| Terms.Var i, Terms.Var j
-	    when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+        | s, t when U.eq_foterm s t -> subst
+        | Terms.Var i, Terms.Var j
+            when (not (List.exists (fun (_,k) -> k=t) subst)) ->
             let subst = Subst.build_subst i t subst in
               subst
-	| Terms.Node l1, Terms.Node l2 -> (
+        | Terms.Node l1, Terms.Node l2 -> (
             try
               List.fold_left2
-		(fun subst' s t -> equiv subst' s t)
-		subst l1 l2
+                (fun subst' s t -> equiv subst' s t)
+                subst l1 l2
             with Invalid_argument _ ->
               raise (UnificationFailure (lazy "Inference.unification.unif"))
           )
-	| _, _ ->
+        | _, _ ->
             raise (UnificationFailure (lazy "Inference.unification.unif"))
     in
       equiv Subst.id_subst s t