From d9e43f0e6d592d6b385b673a3c1dc8e12ca753c4 Mon Sep 17 00:00:00 2001
From: Doug Woos <doug.woos@gmail.com>
Date: Tue, 31 Jan 2017 11:47:44 -0800
Subject: [PATCH] use insert_if_not_there

---
 src/tactic/sine_filter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index f5ecc36a3..71ae58f8c 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -98,8 +98,8 @@ private:
             if (is_app(curr)) {
                 app *a = to_app(curr);
                 func_decl *f = a->get_decl();
-                if (is_name(f) && !consts.contains(f)) {
-                    consts.insert(f);
+                if (is_name(f)) {
+                    consts.insert_if_not_there(f);
                 }
             }
         }