[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

[Lars Hupel]

Dear list,

since Isabelle/af2d0e07493b, presenting the HOL-Hoare session fails:

*** Incoherent use of file name "hoare_syntax.ML" as 
"files/hoare_syntax.ML.html" in theory HOL-Hoare.Hoare_Logic vs. 
HOL-Hoare.Hoare_Logic_Abort

The first failing build log is:

<https://ci.isabelle.systems/jenkins/job/isabelle-all/2543/consoleFull>

Based on my superficial understanding, this problem appears to be caused 
by two different theories including the same ML file 
(src/HOL/Hoare/hoare_syntax.ML).

Since the ML file is dependent on syntax that is independently 
introduced by those theories, I'm unsure how to fix this. The naive 
solution would be to duplicate the ML file, but that seems inelegant.

Happy holidays,
Lars