X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoSubst.ml;h=2d63d34afca2372e1c49f9dcea9c1f44959b17b7;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=5cb84e1c938d1ff20b359bc738f7f0b713cfe87f;hpb=eca915d2656084f1e58149a476a2d305758b00f9;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 5cb84e1c9..2d63d34af 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -36,6 +36,17 @@
       varlist
   ;;
 
+  let rec reloc_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> 
+        (try
+           List.assoc i subst
+         with
+             Not_found -> assert false)
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> reloc_subst subst t) l)
+;;
+
   let rec apply_subst subst = function
     | (Terms.Leaf _) as t -> t
     | Terms.Var i ->