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

[Makarius]

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.


 	Makarius