# HG changeset patch
# User wenzelm
# Date 1514460052 -3600
# Node ID e67abae0e1ca3fcb3b464bcbb3448cefab80023e
# Parent  0094d938c53b765e22da0cfd4ed2bc13cb5f4741
unused;

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";