[isabelle] Problem with quickcheck in Isabelle2015

Dear all Isabelle users,

I have the following strange behavior of quickcheck on the following simple theory:

datatype t= A | B "(t list)"

value "B [A,A]"

fun f:: "t â bool"
"f _= True"

lemma "f (x::t)= True"
quickcheck [tester=narrowing]

All the quickcheck calls fail. The last one fails with the following error message:

Type unification failed: No type arity t :: narrowing

Type error in application: incompatible operand type

Operator:  ??.Quickcheck_Narrowing.ensure_testable :: ??'a â ??'a
Operand:   Îx. equal_bool_inst.equal_bool (f x) True :: t â bool

Note that the same example works fine with Isabelle2012.

Thanks in advance for any hint,

Best regards,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr

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