diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 4022b1402..2946bb1bc 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -437,10 +437,6 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
 }
 
 
-app* seq_util::str::mk_string(symbol const& s) {
-    return u.seq.mk_string(s);
-}
-
 void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
     expr* e1, *e2;
     while (is_concat(e, e1, e2)) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index c11f830b4..0ab889c38 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -167,11 +167,11 @@ public:
         ast_manager& m;
         family_id    m_fid;
     public:
-        str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
+        str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
 
         sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
         app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
-        app* mk_string(symbol const& s);
+        app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
         app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
         app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
@@ -229,11 +229,10 @@ public:
     };
 
     class re {
-        seq_util&    u;
         ast_manager& m;
         family_id    m_fid;
     public:
-        re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
+        re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
 
         bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }