From d61e6fdd8906397f7aa03b509cab03bcd82393d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Oct 2014 15:21:08 -0700
Subject: [PATCH] refactor(frontends/lean/util): add auxiliary function

---
 src/frontends/lean/decl_cmds.cpp     | 2 +-
 src/frontends/lean/inductive_cmd.cpp | 2 +-
 src/frontends/lean/util.h            | 3 +++
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 1c911642c..21faaaf72 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -378,7 +378,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
         levels section_ls = collect_section_nonvar_levels(p, ls);
         remove_section_variables(p, section_ps);
         if (!section_ps.empty()) {
-            expr ref = mk_section_local_ref(real_n, section_ls, section_ps.size(), section_ps.data());
+            expr ref = mk_section_local_ref(real_n, section_ls, section_ps);
             p.add_local_expr(n, ref);
         } else if (section_ls) {
             expr ref = mk_constant(real_n, section_ls);
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index ac82376eb..2b90632d4 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -594,7 +594,7 @@ struct inductive_cmd_fn {
         else
             id = name(full_id.get_string());
         if (in_section_or_context(env)) {
-            expr r = mk_section_local_ref(full_id, section_levels, section_params.size(), section_params.data());
+            expr r = mk_section_local_ref(full_id, section_levels, section_params);
             m_p.add_local_expr(id, r);
         }
         if (full_id != id)
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 6fd0f6bd8..6634d8ac0 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -36,6 +36,9 @@ list<expr> locals_to_context(expr const & e, parser const & p);
     That is, when the user writes \c n inside the section she is really getting the term returned by this function.
 */
 expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_sec_params, expr const * sec_params);
+inline expr mk_section_local_ref(name const & n, levels const & sec_ls, buffer<expr> const & sec_params) {
+    return mk_section_local_ref(n, sec_ls, sec_params.size(), sec_params.data());
+}
 /** \brief Return true iff \c e is a term of the form
     <tt>(@^-1 (@n.{ls} @l_1 ... @l_n))</tt> where
     \c n is a constant and l_i's are local constants.