# [isabelle] Export from class target fails to replace operations

Dear experts of the type class implementation,

`I have the following problem. In one theory, a constant (fractrel) is defined in the
``target of a type class (idom) and the definition depends on some of the parameters of the
``type class. In another theory, a subclass (euclidean_ring) of this type class is defined.
``In a third theory, which imports both theories, I prove in the type class target of the
``subclass a lemma which refers to the constant fractrel.
`

`After having left the type class target, I found that the theorem is not exported
``correctly. The theorem refers to the foundational constant "idom.fractrel ..." rather than
``the overloaded constant "fractrel".
`
Here is a minimal example:
theory Scratch imports Main begin
definition (in idom) fractrel :: "'a Ã 'a â 'a * 'a â bool"
where "fractrel = (Îx y. fst x * snd y = fst y * snd x)"
end
theory ScratchA imports Scratch "~~/src/HOL/Number_Theory/Euclidean_Algorithm" begin
lemma (in euclidean_ring) lem: "b â 0 â fractrel (a, b) (a, b)" sorry
thm lem
end
The "thm lem" command outputs
?b â 0 â idom.fractrel op * (?a, ?b) (?a, ?b)
but it should be
?b â 0 â fractrel (?a, ?b) (?a, ?b)

`Obviously, lem in the current form is unusable, because "idom.fractrel op *" and
``"fractrel" do not unify. What is going on here or am I doing something wrong? How do I get
``the theorem I'd like to have?
`
Best,
Andreas

`PS: In my actual use case, the lemma lem refers to a constant defined in the context of
``euclidean_ring, so I cannot just move it to the target idom, where the export from the
``context works as expected. Also, the definition of fractrel should be in some other theory
``than the lemma; if they were in the same, the export works again as expected.
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*