X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=eca23e720dd9909f23ce10e2004ce6023d649470;hb=016f069da6221053873b4d505716ef1bd80f08b6;hp=c1d5f8bdcffcd9ab3d7a2f226a278e0afe4c6440;hpb=b69275324ae2d436f2f4dbb70e0ddcbdf3886636;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c1d5f8bdc..eca23e720 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -98,14 +98,6 @@ module Superposition (B : Terms.Blob) =
       in
         aux bag pos ctx id t
     ;;
-
-    let vars_of_term t =
-      let rec aux acc = function
-	| Terms.Leaf _ -> acc
-	| Terms.Var i -> if (List.mem i acc) then acc else i::acc
-	| Terms.Node l -> List.fold_left aux acc l
-      in aux [] t
-    ;;
     
     let build_clause bag filter rule t subst vl id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
@@ -119,7 +111,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
+          Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
         in
         Some (bag, uc)
       else