From 8d51607ea0e4b0548ba9aff7eff8cbb0b37e4967 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Sep 2016 18:14:53 -0700
Subject: [PATCH] chore(frontends/lean/elaborator): remove verbose trace
 message

---
 src/frontends/lean/elaborator.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 47e95a58a0..7e491e6bd3 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1053,9 +1053,6 @@ expr elaborator::visit_default_app_core(expr const & _fn, arg_mask amask, buffer
 
     expr r = mk_app(fn, new_args.size(), new_args.data());
     if (expected_type) {
-        trace_elab_debug(tout() << "application\n  " << r << "\nhas type\n  " <<
-                         type << "\nexpected\n  " << *expected_type << "\nfunction type:\n  " <<
-                         fn_type << "\n";);
         if (auto new_r = ensure_has_type(r, instantiate_mvars(type), *expected_type, ref)) {
             return *new_r;
         } else {