duplicate entry in menv avoided

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index c8ab4e428cfecdc9f9e92f672b55fdb532b00f52..7cb9fb0e5bc9beb8b523ae42cbcdaf8720c9828b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1623,7 +1623,12 @@ let all_subsumed bag maxm status active passive =
                status goalproof newproof subsumption_id subsumption_subst proof_menv
           in
           let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
-          let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+           let newmetasenv = 
+             other_menv @ 
+             List.filter
+               (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+           in
+          let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
             (subst, proof,gl)) subsumed_or_id 
   in 
   res, !maxmeta