diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/setup.ML
--- a/doc-src/IsarImplementation/Thy/setup.ML	Thu Aug 31 17:33:55 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/setup.ML	Thu Aug 31 18:27:40 2006 +0200
@@ -33,6 +33,7 @@
   ("index_ML_type", arguments (index_ml "type" ml_type)),
   ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
   ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
+  ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
   ("verbatim", O.args (Scan.lift Args.name) output_verbatim)];
 
 in val _ = () end;