| changeset 67285 | e67abae0e1ca |
| parent 67263 | 449a989f42cd |
| child 67297 | 86a099f896fc |
--- 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";