fix(util/trie): compilation issue

See #1619
leanprover · Jun 16, 2017 · d38979f · d38979f
1 parent 3e429f0
commit d38979f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/util/trie.h b/src/util/trie.h
@@ -66,7 +66,7 @@ class trie : public KeyCMP {
                 } else {
                     trie n1(*c1);
                     new_t1->m_children.erase(k);
-                    new_t1->m_children.insert(k, merge(n1.steal(), c2));
+                    new_t1->m_children.insert(k, trie::merge(n1.steal(), c2));
                 }
             });
         return new_t1;