X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUtils.ml;h=10c96f543578f2133898f2077323f85cc1483855;hb=9883f04161a9972f0641dd85faf224b4f2846f05;hp=454432ec48925a4e53dc734aa6680faff7e14d7f;hpb=a6011d00d7c377056ead2e0974c68a7a3ae069d0;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 454432ec4..10c96f543 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -72,15 +72,15 @@ module Utils (B : Terms.Blob) = struct
   let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
   let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
     
-  let relocate maxvar varlist =
+  let relocate maxvar varlist subst =
     List.fold_right
       (fun i (maxvar, varlist, s) -> 
          maxvar+1, maxvar::varlist, Subst.build_subst i (Terms.Var maxvar) s)
-      varlist (maxvar+1, [], Subst.id_subst)
+      varlist (maxvar+1, [], subst)
   ;;
 
   let fresh_unit_clause maxvar (id, lit, varlist, proof) =
-    let maxvar, varlist, subst = relocate maxvar varlist in
+    let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
     let lit = 
       match lit with
       | Terms.Equation (l,r,ty,o) ->