snapshot

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

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index bfef2f2b176d531f385bf782bf1cc9fed0271397..9053ec223a3a25fcac036746bb30e1e4bd5ea49d 100644 (file)
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -38,7 +38,10 @@ 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)
 ;;