diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 46aa8b8558..77b0bfde91 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -288,7 +288,7 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & if (r_congr_hyp.has_proof()) simplified = true; - lean_assert(is_meta(h_rhs)); + lean_assert(is_metavar_app(h_rhs)); buffer new_val_meta_args; expr new_val_meta = get_app_args(h_rhs, new_val_meta_args); lean_assert(is_metavar(new_val_meta));