Lean4Repl.lean fails on newer Lean versions (missing Std.TreeSet.union)

[lllx125]

Description
I am encountering a build error when using lean_dojo with a repo. The error message is

Lean4Repl.lean:121:21: Invalid field `union`: The environment does not contain `Std.TreeSet.union`

where it is in fact NameSet.union that doesn't exist, Here is the code snippet from Lean4Repl.lean:121.

private def collectFromLevel : Level → NameSet
| Level.zero => NameSet.empty
| Level.succ l => collectFromLevel l
| Level.param n => NameSet.empty.insert n
| Level.max l1 l2 => (collectFromLevel l1).union $ collectFromLevel l2
| Level.imax l1 l2 => (collectFromLevel l1).union $ collectFromLevel l2
| Level.mvar _ => NameSet.empty

I believe this is due to recent upgrade where NameSet is defined as TreeSet in src/Lean/Data/NameMap/Basic.lean. They removed the RBTree definition and changed to TreeSet, which does not have .union