cannot create same-name record and field in different theory

[xrchz]

I'm not sure whether this is intentional, but I would prefer if this were allowed (or to know the rationale for disallowing it):
fooScript.sml:

open HolKernel bossLib;
val _ = new_theory"foo";
val _ = Datatype`foo = <| f : bool |>`;
val _ = export_theory();

barScript.sml:

open HolKernel bossLib fooTheory;
val _ = new_theory"bar";
val _ = Datatype`foo = <| f : bool |>`;
val _ = export_theory();

Exception raised at Datatype.Hol_datatype:
at Term.create_const:
not a type match
Exception- HOL_ERR {message = "at Term.create_const:\nnot a type match", origin_function = "Hol_datatype", origin_structure = "Datatype"} raised
Holmake: Failed script build for barScript - exited with code 1

[mn200]

It should be allowed. Curiously, though I get warning messages when I try this, I don't get failures. I will commit my test-case (and try to make the code more robust such that it doesn't give me mk_const warnings; what the heck is create_const?)

[xrchz]

I saw the exception on 1ee64d3. I'll try updating to see if it turns into just a warning...

[xrchz]

still get the exception at HEAD (abc8e74)

[mn200]

Can you adjust the test-case so as to demonstrate the bug please? I still can't reproduce (and nor can the regression machines so far).

[mn200]

Don't worry; I've got a local reproduction.