src/Pure/Thy/ROOT.ML

--- a/src/Pure/Thy/ROOT.ML	Thu Oct 26 13:53:00 1995 +0100
+++ b/src/Pure/Thy/ROOT.ML	Thu Oct 26 13:53:04 1995 +0100
@@ -38,7 +38,7 @@
                                    \and ThmDB = ThmDB);",
     "ReadThy.loaded_thys := !loaded_thys;",
     "ReadThy.gif_path := !gif_path;",
-    "ReadThy.chart00_path := !chart00_path;",
+    "ReadThy.index_path := !index_path;",
     "ReadThy.make_html := !make_html;",
     "ThmDB.thm_db := !thm_db;",
     "open ThmDB ReadThy;"];