On 01/28/2015 06:15 PM, Florian Haftmann wrote:
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+ Config.get ctxt show_variants orelse
+ exists (can Term.type_of) ts then ts
else map (insert_overloaded ctxt) ts;
Nb. is_none o try f <--> not o can f
This got swapped in this patch and is maybe the reason for failing to
solve the problem.
Cheers,
Florian
Thanks for pointing this out. While yours is a valid observation, it
seems that observing "abbrev_mode" is not enough to obtain nicer output,
i.e., when using
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try
Term.type_of) ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+ Config.get ctxt show_variants orelse
+ exists (not o can Term.type_of) ts then ts
else map (insert_overloaded ctxt) ts;
instead of the above, the output of
term "xs ≤⇩♯ ys"
stays the same as in my initial post, namely
"Foo.le_sharp ♯ xs ys"
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
