Removed unused parameter of unification procedure (vars)

[helm.git] / helm / software / components / ng_paramodulation / foUnif.ml

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 427db4f95bfca6c911bb5b1f6d9cf5dd786430ef..cb3045c1918e9b0c9682e68c939440eb061d5c10 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -29,7 +29,7 @@ module Founif (B : Orderings.Blob) = struct
   module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
-  let unification vars locked_vars t1 t2 =
+  let unification (* vars *) locked_vars t1 t2 =
     let rec occurs_check subst what where =
       match where with
       | Terms.Var i when i = what -> true