X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoSubst.ml;h=5cb84e1c938d1ff20b359bc738f7f0b713cfe87f;hb=047a0464181070aa816c189c7a6dd5ebeb68bc45;hp=6154306b5e1d9959fc5ee7ec2d0facb51d80f119;hpb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 6154306b5..5cb84e1c9 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -15,16 +15,16 @@
   
   let build_subst n t tail = (n,t) :: tail ;;
   
-  let rec lookup_subst var subst =
+  let rec lookup var subst =
     match var with
       | Terms.Var i ->
           (try
-            lookup_subst (List.assoc i subst) subst
+            lookup (List.assoc i subst) subst
           with
               Not_found -> var)
       | _ -> var
   ;;
-  let lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
+  let lookup i subst = lookup (Terms.Var i) subst;;
   
   let is_in_subst i subst = List.mem_assoc i subst;;
   
@@ -39,7 +39,7 @@
   let rec apply_subst subst = function
     | (Terms.Leaf _) as t -> t
     | Terms.Var i -> 
-        (match lookup_subst i subst with
+        (match lookup i subst with
         | Terms.Node _ as t -> apply_subst subst t
         | t -> t)
     | (Terms.Node l) ->