diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h
index 138d5abee..37a5b8a6c 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.h
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h
@@ -26,8 +26,9 @@ Revision History:
 #define _DL_MK_QUANTIFIER_INSTANTIATION_H_
 
 
-#include"dl_rule_transformer.h"
-#include"expr_safe_replace.h"
+#include "dl_rule_transformer.h"
+#include "expr_safe_replace.h"
+#include "union_find.h"
 
 
 namespace datalog {
@@ -37,75 +38,12 @@ namespace datalog {
     class mk_quantifier_instantiation : public rule_transformer::plugin {
         typedef svector<std::pair<expr*,expr*> > term_pairs;
 
-        class union_find {
-            unsigned_vector   m_find;
-            unsigned_vector   m_size;
-            unsigned_vector   m_next;
-
-            void ensure_size(unsigned v) {
-                while (v >= get_num_vars()) {
-                    mk_var();
-                }
-            }
-        public:
-            unsigned mk_var() {
-                unsigned r = m_find.size();
-                m_find.push_back(r);
-                m_size.push_back(1);
-                m_next.push_back(r);
-                return r;
-            }
-            unsigned get_num_vars() const { return m_find.size(); }
-            
-            unsigned find(unsigned v) const {
-                if (v >= get_num_vars()) {
-                    return v;
-                }
-                while (true) {
-                    unsigned new_v = m_find[v];
-                    if (new_v == v)
-                        return v;
-                    v = new_v;
-                }
-            }
-            
-            unsigned next(unsigned v) const { 
-                if (v >= get_num_vars()) {
-                    return v;
-                }
-                return m_next[v]; 
-            }
-            
-            bool is_root(unsigned v) const { 
-                return v >= get_num_vars() || m_find[v] == v; 
-            }
-            
-            void merge(unsigned v1, unsigned v2) {
-                unsigned r1 = find(v1);
-                unsigned r2 = find(v2);
-                if (r1 == r2)
-                    return;
-                ensure_size(v1);
-                ensure_size(v2);
-                if (m_size[r1] > m_size[r2])
-                    std::swap(r1, r2);
-                m_find[r1] = r2;
-                m_size[r2] += m_size[r1];
-                std::swap(m_next[r1], m_next[r2]);
-            }
-
-            void reset() {
-                m_find.reset();
-                m_next.reset();
-                m_size.reset();
-            }
-        };
 
         ast_manager&      m;
         context&          m_ctx;
         expr_safe_replace m_var2cnst; 
         expr_safe_replace m_cnst2var;
-        union_find        m_uf;
+        basic_union_find  m_uf;
         ptr_vector<expr>  m_todo;
         ptr_vector<expr>  m_terms;
         ptr_vector<expr>  m_binding;
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 32de6846a..23d33a442 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -173,5 +173,71 @@ public:
 #endif
 };
 
+
+class basic_union_find {
+    unsigned_vector   m_find;
+    unsigned_vector   m_size;
+    unsigned_vector   m_next;
+    
+    void ensure_size(unsigned v) {
+        while (v >= get_num_vars()) {
+            mk_var();
+        }
+    }
+ public:
+    unsigned mk_var() {
+        unsigned r = m_find.size();
+        m_find.push_back(r);
+        m_size.push_back(1);
+        m_next.push_back(r);
+        return r;
+    }
+    unsigned get_num_vars() const { return m_find.size(); }
+    
+    unsigned find(unsigned v) const {
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        while (true) {
+            unsigned new_v = m_find[v];
+            if (new_v == v)
+                return v;
+            v = new_v;
+        }
+    }
+    
+    unsigned next(unsigned v) const { 
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        return m_next[v]; 
+    }
+    
+    bool is_root(unsigned v) const { 
+        return v >= get_num_vars() || m_find[v] == v; 
+    }
+    
+    void merge(unsigned v1, unsigned v2) {
+        unsigned r1 = find(v1);
+        unsigned r2 = find(v2);
+        if (r1 == r2)
+            return;
+        ensure_size(v1);
+        ensure_size(v2);
+        if (m_size[r1] > m_size[r2])
+            std::swap(r1, r2);
+        m_find[r1] = r2;
+        m_size[r2] += m_size[r1];
+        std::swap(m_next[r1], m_next[r2]);
+    }
+    
+    void reset() {
+        m_find.reset();
+        m_next.reset();
+        m_size.reset();
+    }
+};
+
+
 #endif /* _UNION_FIND_H_ */