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

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index aab240168..5cb84e1c9 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -36,17 +36,6 @@
       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 -> 
@@ -57,10 +46,6 @@
 	Terms.Node (List.map (fun t -> apply_subst subst t) l)
 ;;
 
-  let flat subst =
-    List.map (fun (x,t) -> (x, apply_subst subst t)) subst
-;;
-
   let concat x y = x @ y;;
   
 (* end *)