From 1bb5b2ec01d27460327c66301b462df0c00a350e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Jan 2017 13:48:11 -0800
Subject: [PATCH] feat(library/tactic/simp_lemmas): do not pretty print bizarre
 "perm" flag

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

diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 7d4c43a958..f6b62dd3fc 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -187,8 +187,10 @@ format simp_lemma::pp(formatter const & fmt) const {
         r += space() + paren(format(get_priority()));
     if (is_refl())
         r += space() + format("defeq");
+    /*
     if (is_permutation())
         r += space() + format("perm");
+    */
     if (kind() == simp_lemma_kind::Congr) {
         format r1;
         for (expr const & h : get_congr_hyps()) {