# [isabelle] Type class instantiation without using Isar syntax

Hi,
I have recently migrated to Isabelle 2009. I have a Haskell code base that
produces Isabelle code automatically, however it does not produce Isar code.
Since the migration to Isabelle 2009, my instantiation of the Quotient class
does not work, where it used to work in 2008.
Could someone please help me with the code below and show me the new correct
syntax in plain Isabelle. Once this goes through then I will be able to
apply the same syntax to my Haskell code base (currently migrating the
codebase to Isar is far too much work and I don't have the time).
The error I get is on the defs line. The error is:
*** Clash of specifications "test.myType_sim_def" and
"test.eqv_MyType_inst.eqv_MyType_def" for constant "Quotient.eqv_class.eqv"
*** The error(s) above occurred in definition "myType_sim_def":
*** "x ~ y == eq x y"
*** At command "defs".
Any help will be most appreciated.
Thanks
Liam
The sample file I am working with is
--------------------
theory test
imports Main "Quotient"
begin
datatype MyType = A | B
consts
eq :: "MyType => MyType => bool"
primrec "eq A y = (y = A)"
"eq B y = (y = B)"
instance MyType:: eqv
by (intro_classes)
defs (overloaded)
myType_sim_def : "eqv x y == (eq x y)"
instance MyType:: equiv
apply (intro_classes)
apply (unfold myType_sim_def)
apply (auto)
done
end

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