diff -r 0242c9c980df -r a31203f58b20 doc-src/IsarRef/Thy/ML_Tactic.thy
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Thu May 08 22:05:15 2008 +0200
@@ -4,7 +4,7 @@
 imports Main
 begin
 
-chapter {* ML tactic expressions \label{sec:conv-tac} *}
+chapter {* ML tactic expressions *}
 
 text {*
   Isar Proof methods closely resemble traditional tactics, when used