From e41c4d384dccf96d7118858fd0bbc97827fbfeff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 1 Jul 2017 12:17:53 -0700
Subject: [PATCH] chore(library/tactic/simp_lemmas): remove unnecessary whnf

---
 src/library/tactic/simp_lemmas.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index eb233bfbb4..4c1daa37a0 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -685,7 +685,7 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
            universe metavariables in this loop. */
         ctx.resize_tmp_mvars(_emetas.size());
         expr rule  = ctx.whnf(p.first);
-        expr proof = ctx.whnf(p.second);
+        expr proof = p.second;
         bool is_perm = is_permutation_ceqv(env, rule);
         buffer<expr> emetas;
         emetas.append(_emetas);