diff --git a/src/api/decl.cpp b/src/api/decl.cpp
index 23b677eeff..dcf680e9d4 100644
--- a/src/api/decl.cpp
+++ b/src/api/decl.cpp
@@ -58,7 +58,7 @@ lean_bool lean_decl_mk_thm(lean_name n, lean_list_name p, lean_expr t, lean_expr
     LEAN_CATCH;
 }
 
-lean_bool lean_decl_mk_thm(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex) {
+lean_bool lean_decl_mk_thm_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(e);
     check_nonnull(n);
diff --git a/src/api/lean_env.h b/src/api/lean_env.h
index 1f641ce07d..e787a0e103 100644
--- a/src/api/lean_env.h
+++ b/src/api/lean_env.h
@@ -68,7 +68,7 @@ lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex);
     \remark Every declaration passed to \c f must be disposed using \c lean_decl_del. */
 lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex);
 /** \brief Execute \c f for each global universe in \c env.
-    \remark Every name passed to \c f must be disposed using \c lean_nam_del. */
+    \remark Every name passed to \c f must be disposed using \c lean_name_del. */
 lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex);
 /*@}*/
 /*@}*/