Snippet does not work with latest lean 2

[gebner]

There is at least one snippets that does not work with the current lean 2 version, in 10_Structures_and_Records.org:

import standard
open nat

structure big :=
(field1 : nat) (field2 : nat)
(field3 : nat) (field4 : nat)
(field5 : nat) (field6 : nat)

definition b : big := big.mk 1 2 3 4 5 6

definition v3 : nat :=
match b with
{| big, field3 := v |} := v
end

example : v3 = 3 := rfl

which fails with

10_Structures_and_Records.org.11.lean:13:3: error: invalid structure instance, given type is not a structure
[...]

This is also broken with the lean.js version used by the online tutorial.

[avigad]

Interesting -- I wonder when it broke. This works instead:

definition v3 : nat :=
  match b with
   big.mk _ _ v _ _ _ := v
  end

I don't know when anyone has ever the structure notation in a match.

@leodemoura Should I just remove this from the Lean 2 tutorial?