[isabelle-dev] Building the IsarImplementation Manual on 9fc17f9ccd6c

[Lukas Bulwahn]

I cannot build the IsarImplementation Manual on 9fc17f9ccd6c:
Maybe some latest change broke the document generation.

Lukas


Running HOL-Thy ...
HOL-Thy FAILED
(see also 
/home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy)

***
*** The error(s) above occurred in document antiquotation: 
"Base.index_ML" (line 130 of "~~/doc-src/IsarImplementation/Thy/Logic.thy")
*** At command "text" (line 118 of 
"~~/doc-src/IsarImplementation/Thy/Logic.thy")
*** Error:
*** Type mismatch in type constraint.
***    Value: Name_Space.declare :
***       Context.generic ->
***       bool -> binding -> Name_Space.T -> string * Name_Space.T
***    Constraint:
***    Proof.context ->
***    bool ->
***    Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T
***    Reason:
***    Can't unify Context.generic with Proof.context
***       (Different type constructors)
***
*** The error(s) above occurred in document antiquotation: 
"Base.index_ML" (line 1109 of 
"~~/doc-src/IsarImplementation/Thy/Prelim.thy")
*** At command "text" (line 1089 of 
"~~/doc-src/IsarImplementation/Thy/Prelim.thy")
Exception- TOPLEVEL_ERROR raised
*** ML error

make: *** 
[/home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy.gz] 
Error 1