diff -r fb31b7a6c858 -r 715178f6ae31 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:41:21 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:54:37 2008 +0100
@@ -812,6 +812,7 @@
   'sledgehammer' (nameref *)
   ;
   'atp\_messages' ('(' nat ')')?
+  ;
 
   'metis' thmrefs
   ;