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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
