diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 799fec5257..68f85c34a2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3277,12 +3277,13 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
                                              mk_lean_list(new_try_args))));
         }
     }
-    struc << "instance " << macro.to_string() << ".has_view : has_view " << esc_macro.to_string() << " " << macro.to_string() << ".view :=\n"
+    struc << "def " << macro.to_string() << ".has_view' : has_view " << esc_macro.to_string() << " " << macro.to_string() << ".view :=\n"
             << "{ view := fun stx, let stxs : list syntax := match stx with"
             << "| syntax.node (syntax_node.mk " << esc_macro.to_string() << " stxs) := stxs | _ := [] in\n"
             << binds.str()
             << macro.to_string() << ".view.mk " << mk_args.str() << ",\n"
             << "review := fun ⟨" << view_pat.str() << "⟩, syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << reviews.str() << "]) }";
+    struc << "instance " << macro.to_string() << ".has_view := " << macro.to_string() << ".has_view'";
     trace_elab_detail(tout() << "expansion of node! macro:\n" << struc.str(););
     std::istringstream in(struc.str());
     parser p(m_env, get_global_ios(), in, "foo");
@@ -3290,6 +3291,7 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
     p.parse_command_like();
     p.parse_command_like();
     p.parse_command_like();
+    p.parse_command_like();
     m_env = p.env();
     m_ctx.set_env(m_env);
     return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}), mk_const(get_namespace(p.env()) + macro), mk_lean_list(new_args)),
@@ -3346,7 +3348,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
         i++;
         new_args.push_back(mk_as_is(r));
     }
-    struc << "instance " << macro.to_string() << ".has_view : has_view " << esc_macro.to_string() << " "
+    struc << "def " << macro.to_string() << ".has_view' : has_view " << esc_macro.to_string() << " "
           << macro.to_string() << ".view :=\n"
           << "{ view := fun stx, let (stx, i) := match stx : _ -> prod syntax nat with \n"
           << "| syntax.node (syntax_node.mk " << esc_macro.to_string()
@@ -3358,6 +3360,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
           << " [match v with\n"
           << review_cases.str()
           << "]) }";
+    struc << "instance " << macro.to_string() << ".has_view := " << macro.to_string() << ".has_view'";
     trace_elab_detail(tout() << "expansion of node_choice! macro:\n" << struc.str(););
     std::istringstream in(struc.str());
     parser p(m_env, get_global_ios(), in, "foo");
@@ -3365,6 +3368,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
     p.parse_command_like();
     p.parse_command_like();
     p.parse_command_like();
+    p.parse_command_like();
     m_env = p.env();
     m_ctx.set_env(m_env);
     return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}),