X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoSubst.ml;h=6154306b5e1d9959fc5ee7ec2d0facb51d80f119;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=bfef2f2b176d531f385bf782bf1cc9fed0271397;hpb=d6139bbb7c5e20f8139231a90435b8b82a0438ef;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index bfef2f2b1..6154306b5 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module Subst (B : Terms.Blob) = struct
+(* module Subst (B : Terms.Blob) = struct *)
   
   let id_subst = [];;
   
@@ -38,11 +38,14 @@ module Subst (B : Terms.Blob) = struct
 
   let rec apply_subst subst = function
     | (Terms.Leaf _) as t -> t
-    | Terms.Var i -> lookup_subst i subst
+    | 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
+(* end *)