From 468e3b35a467e49edb8e5e83469d24520aff83ee Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Jul 2005 12:13:16 +0000
Subject: [PATCH] Cosmetic changes: a piece of code replaced with a pre-defined
 function.

---
 helm/ocaml/tactics/equalityTactics.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 7eae7fb5c..99bfd2081 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -103,11 +103,9 @@ let rewrite_tac ~direction ~pattern equality =
       (PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
   in
   assert (List.length goals = 0) ;
-  let goals = List.map (fun (i,_,_) -> i) metasenv' in
   let goals =
-   List.filter
-    (fun i ->
-      not (List.exists (fun (j,_,_) -> i=j) metasenv)) goals
+   ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+    ~newmetasenv:metasenv'
   in
    (proof',goals)
  in
-- 
2.39.2