[isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]

[Christian Sternagel]

On 09/30/2013 07:33 PM, Makarius wrote:
> On Tue, 24 Sep 2013, Christian Sternagel wrote:
>
>> After this changeset, variants may be arbitrary terms (due to
>> localization). Now replacing a variant by the corresponding overloaded
>> constant is done by rewriting (as Florian already pointed out, this
>> happens in "insert_overloaded") as follows
>>
>>   fun insert_overloaded ctxt variant =
>>     (case try Term.type_of variant of
>>       NONE => variant
>>     | SOME T =>
>>       Pattern.rewrite_term (Proof_Context.theory_of ctxt) []
>>         [Option.map (Const o rpair T) o
>>         get_overloaded ctxt o Term.map_types (K dummyT)] variant);
>>
>> Apparently this interferes with abbreviations. Am I doing anything
>> strange here?
>
> I've looked only briefly so far.  Abbreviations are only contracted for
> type-correct terms, but above that information is not fully preserved.
>
> Pattern.rewrite_term needs to re-used the type of the replaced subterm
> (within the proc), not the overall type of the term called "variant" above.

Thanks! That's a valuable hint. I will look into it and hope to make 
adhoc overloading and abbreviations produce the expected results again, 
before the release.

cheers

chris

>
>
>      Makarius