[isabelle] Isabelle document prep and ACM journals document class

Dear Isabelle users,

Does anyone on the list have experience preparing documents that use the 
'acmsmall' document class?

I'm getting a latex error when building and am hoping somebody might 
have experience in how to debug or resolve it.

Below is a minimal example, derived by doing a clean 'isabelle mkroot 
-d', with a minimal theory file and the relevant document class and 
associated style files.

In case you want to reproduce, download: 
and extract the 'acmsmall.cls' and 'acmcopyright.sty' files (listed in 
the ROOT file below).

$ cat Test.thy
theory Test
imports Main

text {*
Here is a theorem: @{thm TrueI}

$ ls document/
acmcopyright.sty acmsmall.cls     root.tex

$ head -7 document/root.tex
% the only modification made to the original root.tex generated by
% isabelle mkroot -d


$ cat ROOT
session "minex" = "HOL" +
   options [document = pdf, document_output = "output"]

$ /Applications/Isabelle2016.app/Isabelle/bin/isabelle build -D .
Running minex ...

minex FAILED
(see also 

*** (/usr/local/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty
*** (./root.out) (./root.out)
*** (/usr/local/texlive/2016/texmf-dist/tex/latex/psnfss/ot1phv.fd) 
*** (./session.tex (./Test.tex)
*** Runaway argument?
*** ! File ended while scanning use of \next.
*** <inserted text>
***                 \par
*** l.1 \input{Test.tex}
*** ))
*** ! Emergency stop.
*** <*> \nonstopmode\input{root.tex}
*** !  ==> Fatal error occurred, no output PDF file produced!
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
*** Failed to build document "/Users/tobiasm1/tmp/minex/output/document.pdf"
Unfinished session(s): minex
0:00:08 elapsed time, 0:00:19 cpu time, factor 2.37

Any suggestions would be very helpful and much appreciated.

Thanks heaps


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.