[isabelle] Error: Non-constructor pattern not allowed in sequential mode



Hi everyone,
I just got this error and I don't know how to work around. The code is like
(not exactly):

record Foo =
    x :: "nat"
    y :: "nat"

fun bar :: "Foo => nat => nat"
where
  "bar (| x = n1, y = n2|)  z = compute n1 n2 z"

But it doesn't allow the record pattern there. I got the error
"Non-constructor pattern not allowed in sequential mode".
How can we use record patterns in functions like the one above?

Thank you

Anh




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