invalid structure header

Stream: maths

[Ashvni Narayanan]

import algebra.group.hom

structure monoid_hom' (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]
  extends one_hom M N, mul_hom M N

I copy pasted the definition of monoid_hom in my file. When I run this (not necessarily with the same import), I get the following error :

invalid 'structure' header, field 'to_fun' from 'mul_hom' has already been declared

What am I missing? Any help is appreciated, thank you!

[Johan Commelin]

But set_option old_structure_cmd true above the structure command. It's a technical implementation thingy.

[Ashvni Narayanan]

Great, it works! Thank you!