diff --git a/library/data/lazy_list.lean b/library/data/lazy_list.lean
index 2f98efca32..ac47b4fc1d 100644
--- a/library/data/lazy_list.lean
+++ b/library/data/lazy_list.lean
@@ -29,7 +29,7 @@ def tail : lazy_list α → lazy_list α
 
 def append : lazy_list α → thunk (lazy_list α) → lazy_list α
 | nil        l  := l ()
-| (cons h t) l  := cons h (append (t ()) (l ()))
+| (cons h t) l  := cons h (@append (t ()) l)
 
 def map (f : α → β) : lazy_list α → lazy_list β
 | nil        := nil
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 95aeee2e8a..f568bb22d2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1516,7 +1516,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
             } else if (i < args.size()) {
                 expr expected_type = d;
                 optional<expr> thunk_of;
-                if (!m_in_pattern) thunk_of = is_thunk(d);
+                if (!m_in_pattern && amask == arg_mask::Default) thunk_of = is_thunk(d);
                 if (thunk_of) expected_type = *thunk_of;
                 // explicit argument
                 expr ref_arg = get_ref_for_child(args[i], ref);