diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 8bed5e13a..0ca4274de 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -66,7 +66,7 @@ class blastenv {
             lean_unreachable();
         }
 
-        expr visit_sort(expr const & e) {
+        virtual expr visit_sort(expr const & e) {
             return blast::mk_sort(to_blast_level(sort_level(e)));
         }
 
diff --git a/src/library/blast/infer_type.cpp b/src/library/blast/infer_type.cpp
index ede0eea42..d4d99acc2 100644
--- a/src/library/blast/infer_type.cpp
+++ b/src/library/blast/infer_type.cpp
@@ -338,7 +338,7 @@ static bool assign_mref_core(expr const & ma, expr const & v) {
     //   3. Any local constant occurring in new_v occurs in locals
     //   4. m does not occur in new_v
     bool ok = true;
-    for_each(v, [&](expr const & e, unsigned) {
+    for_each(new_v, [&](expr const & e, unsigned) {
             if (!ok)
                 return false; // stop search
             if (is_href(e)) {