Implemented LPO

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c1d5f8bdcffcd9ab3d7a2f226a278e0afe4c6440..eca23e720dd9909f23ce10e2004ce6023d649470 100644 (file)
--- 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