src/Doc/Datatypes/Datatypes.thy

 
 subsection \<open>Command Syntax
   \label{ssec:datatype-command-syntax}\<close>
 
 subsubsection \<open>\keyw{datatype}
-  \label{sssec:datatype-new}\<close>
+  \label{sssec:datatype}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
   @{command_def "datatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}

 
 subsection \<open>Command Syntax
   \label{ssec:primrec-command-syntax}\<close>
 
 subsubsection \<open>\keyw{primrec}
-  \label{sssec:primrec-new}\<close>
+  \label{sssec:primrec}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
   @{command_def "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}