[isabelle-dev] adhoc overloading: ugly output

[Christian Sternagel]

Dear all,

in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when 
using adhoc overloading together with abbreviations is not optimal 
(maybe this was already discovered before but I forgot about it). Now, 
it turns out that the same issue (at least superficially it's the same, 
but maybe caused by different reasons) arises also for definitions in 
local theory contexts (or are those the same as mere abbreviations?).

Let me illustrate what I'm talking about by the following example:

theory Foo
imports
   Main
   "~~/src/Tools/Adhoc_Overloading"
begin

consts SHARP :: "'a ⇒ 'b" ("♯")

context
   fixes shp :: "'a ⇒ 'a"
begin

adhoc_overloading
   SHARP shp

definition le_sharp (infix "≤⇩♯" 50)
where
   "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"

term "xs ≤⇩♯ ys"
text ‹
   Result in @{term "Foo.le_sharp ♯ xs ys"} instead of
   more desirable @{term "xs ≤⇩♯ ys"}. (The same happens
   when we turn the above definition into an abbreviation.)
›

end

text ‹
   In the "global" theory this also happens, but only for
   abbreviations, not for definitions.
›

definition "shp = id"

adhoc_overloading SHARP shp

definition le_sharp' (infix "≤⇩♯" 50)
where
   "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"

term "xs ≤⇩♯ ys"

end

Unfortunately, at the moment I do not have time to look into adhoc 
overloading myself, but let this thread be a reminder. If anybody else 
can provide explanations/comments/solutions, please go ahead!

cheers

chris