diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index c63eedaca4f..8dc6e4e8446 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -32,7 +32,7 @@ namespace array {
         typedef sat::literal literal;
         typedef sat::bool_var bool_var;
         typedef sat::literal_vector literal_vector;
-        typedef union_find<solver, euf::solver>  array_union_find;
+        typedef union_find<solver>  array_union_find;
 
 
         struct stats {
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 91e485a9f5d..df4e5c9c2e9 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -49,7 +49,7 @@ namespace bv {
         typedef std::pair<numeral, unsigned> value_sort_pair;
         typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-        typedef union_find<solver, euf::solver>  bv_union_find;
+        typedef union_find<solver>  bv_union_find;
         typedef std::pair<theory_var, unsigned> var_pos;
 
         friend class ackerman;
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index b2cbba63b12..1bf4d6073c4 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -36,7 +36,7 @@ namespace dt {
         typedef sat::bool_var bool_var;
         typedef sat::literal literal;
         typedef sat::literal_vector literal_vector;
-        typedef union_find<solver, euf::solver>  dt_union_find;
+        typedef union_find<solver>  dt_union_find;
 
         struct var_data {
             ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched.
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 7e42e1bbad9..0c08ac44623 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -35,7 +35,7 @@ class union_find_default_ctx {
     _trail_stack m_stack;
 };
 
-template<typename Ctx = union_find_default_ctx, typename StackCtx = Ctx>
+template<typename Ctx = union_find_default_ctx>
 class union_find {
     Ctx &                         m_ctx;
     trail_stack &                 m_trail_stack;