diff -r 0094d938c53b -r e67abae0e1ca src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Dec 28 12:13:56 2017 +0100 +++ b/src/Pure/Thy/present.ML Thu Dec 28 12:20:52 2017 +0100 @@ -28,8 +28,6 @@ val html_path = html_ext o Path.basic; val index_path = Path.basic "index.html"; val readme_html_path = Path.basic "README.html"; -val documentN = "document"; -val document_path = Path.basic documentN; val doc_indexN = "session"; val session_graph_path = Path.basic "session_graph.pdf";