[isabelle-dev] adhoc overloading: ugly output

[Christian Sternagel]

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