Proving a type classed theorem in Isabelle

Question

I am to prove a triviality using type classes:

class order =
  fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50)
  assumes refl:    "x ≼ x"
      and trans:   "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
      and antisym: "x ≼ y ⟹ y ≼ x ⟹ x = y"
begin

  theorem "(myle:: ('b::order) ⇒ 'b ⇒ bool) x x"
  proof -
    show ?thesis by (rule refl)
  qed

end

Here, Isabelle/jEdit highlights by (rule refl) in pink and says

Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. myle x x

What is the problem here? Otherwise the proof seems to go through.

Answer 1

myle and ≼ are not the same function.

The type annotation (myle:: ('b::order) ⇒ 'b ⇒ bool) just states that myle is a function that takes two elements of type 'b and returns a boolean and that 'b is a type belonging to the order typeclass.

If you want to prove something about ≼ just use the same symbol or the name lesseq.