[isabelle] Variables in locale assumptions

Dear all,

In Isabelle/jEdit 2013-2, the following locale works fine:

locale Test =
  fixes pred :: "'a set ⇒ 'a rel ⇒ bool"
  assumes a1: "pred S R"
(*  assumes a2: "pred R S" *)
lemma pred_is_UNIV: "pred A B"
  by (metis a1)

However, uncommenting assumption a2 gives me the following error:

Type unification failed
Type error in application: incompatible operand type
Operator:  pred :: 'a set ⇒ ('a × 'a) set ⇒ bool
Operand:   R :: ('a × 'a) set

Page 2 of the locale tutorial seems to suggest that this is a bug. Or should I expect this behaviour?

Thanks in advance!

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