Isabelle and class overloading <p>Two classes are defined containing the same function, but when the two classes is used in a locale there is an unification error:</p> <pre><code>theory Scratch imports Main begin class c1 = fixes getName :: "'a ⇒ string" class c2 = fixes getName :: "'a ⇒ string" locale c12 = fixes match :: "('a::c1) ⇒ ('b::c2) ⇒ bool" assumes as : "match a b ⟶ (getName a) = (getName b)" end </code></pre> <p>The unification error is resolved by renaming (getName b) to (getName_b b) and use the class definition</p> <pre><code> class c2 = fixes getName_b :: "'a ⇒ string" </code></pre> <p>Does a solution exist without renaming?</p> <p><a href="http://stackoverflow.com/questions/15870788/defining-overloaded-constants-in-isabelle">Here</a> a solution is given when the overloading is needed when datatypes are parameters. </p>