[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

On Wed, 4 Nov 2015, Clemens Ballarin wrote:

> On 30 October, 2015 20:02 CET, Makarius <makarius at sketis.net> wrote:
>
>> Standard batch build prints relatively few terms, so this is not yet
>> significant as a test.
>>
>> The following change prints every intermediate Isar toplevel state.  With
>> that I get timeouts or interrupts due to out-of-memory situation in
>> various sessions, e.g. HOL-Nominal-Examples or Jinja.
>
> Unfortunately this already fails without my patch, so it cannot be used 
> as a test.

Odd. I am in the process of looking more closely what really happens here, 
both with and without your change.


 	Makarius