old structure command segfault

Stream: general

[Kevin Buzzard]

import topology.instances.nnreal

set_option old_structure_cmd true

class normed_group (α : Type*) extends add_comm_group α, metric_space α.

-- segfault

In this thread, Christopher Hoskin tries to make a linear ordered add comm group with a norm on it. His way puts two distinct group structures on his type. I tried to fix it like this:

import analysis.normed_space.ordered

universe v

set_option old_structure_cmd true

class linear_ordered_normed_add_comm_group (β : Type v)
  extends linear_ordered_add_comm_group β, normed_group β.

but this doesn't work, because normed_group is defined using the new structure command, and IIRC you can't old_structure_command extend something defined using the new structure command. So I tried to fix this by adding set_option old_structure_cmd true to analysis.normed_space.basic but now I get a segfault in that file.

Am I right in thinking that in Lean 4 Leo banished the old structure command? What are we supposed to be doing in situations such as this now?