From d6139bbb7c5e20f8139231a90435b8b82a0438ef Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Tue, 9 Jun 2009 13:15:58 +0000
Subject: [PATCH] Implemented substitution application and concatenation

---
 helm/software/components/ng_paramodulation/foSubst.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 92d6aba25..bfef2f2b1 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -36,7 +36,13 @@ module Subst (B : Terms.Blob) = struct
       varlist
   ;;
 
-  let apply_subst = assert false;;
-  let concat = assert false
+  let rec apply_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> lookup_subst i subst
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> apply_subst subst t) l)
+;;
+
+  let concat x y = x @ y;;
   
 end
-- 
2.39.2