From 6c07ca5d41e6ae8afd9e04d7cda8e15bfef39030 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Jan 2015 18:57:05 -0800
Subject: [PATCH] perf(library/print): improve is_used_name

---
 src/library/print.cpp                  | 20 ++++++++++++++------
 tests/lean/place_eqn.lean.expected.out |  4 ++--
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/library/print.cpp b/src/library/print.cpp
index ab334c9bfd..915f6823ac 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -16,12 +16,20 @@ Author: Leonardo de Moura
 
 namespace lean {
 bool is_used_name(expr const & t, name const & n) {
-    return static_cast<bool>(
-        find(t, [&](expr const & e, unsigned) {
-                return (is_constant(e) && const_name(e) == n)  // t has a constant named n
-                    || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n
-                    || (is_let(e) && get_let_var_name(e) == n);
-            }));
+    bool found = false;
+    for_each(t, [&](expr const & e, unsigned) {
+            if (found) return false; // already found
+            if ((is_constant(e) && const_name(e) == n)  // t has a constant named n
+                || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n
+                || (is_let(e) && get_let_var_name(e) == n)) {
+                found = true;
+                return false; // found it
+            }
+            if (is_local(e) || is_metavar(e))
+                return false; // do not search their types
+            return true; // continue search
+        });
+    return false;
 }
 
 name pick_unused_name(expr const & t, name const & s) {
diff --git a/tests/lean/place_eqn.lean.expected.out b/tests/lean/place_eqn.lean.expected.out
index 720029ccb2..c277c9841a 100644
--- a/tests/lean/place_eqn.lean.expected.out
+++ b/tests/lean/place_eqn.lean.expected.out
@@ -8,5 +8,5 @@ a : ℕ
 place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
   λ (a : ℕ),
     nat.brec_on a
-      (λ (a_1 : ℕ) (b : nat.below a_1),
-         nat.cases_on a_1 (λ (b_1 : nat.below 0), ?M_1) (λ (a_2 : ℕ) (b_1 : nat.below (succ a_2)), ?M_2) b)
+      (λ (a : ℕ) (b : nat.below a),
+         nat.cases_on a (λ (b : nat.below 0), ?M_1) (λ (a : ℕ) (b : nat.below (succ a)), ?M_2) b)