X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoSubst.ml;h=9053ec223a3a25fcac036746bb30e1e4bd5ea49d;hb=96c91e470f670018df67c9cbff62fa06e3b57c5e;hp=1b9f2624c77760b88f6e59184ecafca0ff12da60;hpb=25cf2297c8d14c14cfb2ff7695c9b6331825f4c9;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 1b9f2624c..9053ec223 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -35,5 +35,17 @@ module Subst (B : Terms.Blob) = struct
          not (is_in_subst m subst))
       varlist
   ;;
+
+  let rec apply_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> 
+        (match lookup_subst i subst with
+        | Terms.Node _ as t -> apply_subst subst t
+        | t -> t)
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> apply_subst subst t) l)
+;;
+
+  let concat x y = x @ y;;
   
 end