diff --git a/src/library/compiler/rec_fn_macro.cpp b/src/library/compiler/rec_fn_macro.cpp
index 395e5d7ea6..b05dbf2635 100644
--- a/src/library/compiler/rec_fn_macro.cpp
+++ b/src/library/compiler/rec_fn_macro.cpp
@@ -78,11 +78,6 @@ name const & get_rec_fn_name(expr const & e) {
     return static_cast<rec_fn_macro_definition_cell const*>(macro_def(e).raw())->get_rec_fn_name();
 }
 
-expr const & get_rec_fn_type(expr const & e) {
-    lean_assert(is_rec_fn_macro(e));
-    return macro_arg(e, 0);
-}
-
 void initialize_rec_fn_macro() {
     g_rec_fn_macro_id = new name("rec_fn");
     g_rec_fn_opcode   = new std::string("RecFn");
diff --git a/src/library/compiler/rec_fn_macro.h b/src/library/compiler/rec_fn_macro.h
index 93d0757600..69537b719b 100644
--- a/src/library/compiler/rec_fn_macro.h
+++ b/src/library/compiler/rec_fn_macro.h
@@ -16,7 +16,6 @@ expr mk_rec_fn_macro(name const & fn_name, expr const & type);
 
 bool is_rec_fn_macro(expr const & e);
 name const & get_rec_fn_name(expr const & e);
-expr const & get_rec_fn_type(expr const & e);
 
 void initialize_rec_fn_macro();
 void finalize_rec_fn_macro();