<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><blockquote type="cite" class=""><div class="">On 7 Jun 2015, at 07:38, Dmitriy Traytel <<a href="mailto:traytel@in.tum.de" class="">traytel@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="font-family: LucidaGrande; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); float: none; display: inline !important;" class="">I'm not sure if this is something for the repository though, since it has a factor of >2 impact on the build-time:</span><br style="font-family: LucidaGrande; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""></div></blockquote></div><br class=""><div class="">Thanks for investigating. But how do we explain this?</div><div class=""><br class=""></div><div class="">Possibly “fun” insists on converting on creating unconditional patterns only, while “recdef” allows conditional equations. But one could easily insert conditions manually in order to simplify the set of patterns. There are 14 instances of recdef in Cooper.thy. Do any of them stand out as extra slow?</div><div class=""><br class=""><div apple-content-edited="true" class=""><span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-size: 11px; border-spacing: 0px;">Larry</span></div><br class=""><div><blockquote type="cite" class=""></blockquote></div></div></body></html>