diff -r 3d3d6038bdaa -r a16b18fd6299 doc-src/IsarImplementation/Thy/ROOT.ML
--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Fri Oct 22 20:43:48 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Fri Oct 22 20:51:45 2010 +0100
@@ -4,7 +4,6 @@
   "Local_Theory",
   "Logic",
   "ML",
-  "ML_old",
   "Prelim",
   "Proof",
   "Syntax",