# HG changeset patch
# User blanchet
# Date 1459237779 -7200
# Node ID 69e4a4fffea99f6ff88a80a49d489e87d13dfdff
# Parent  628c97d39627c0da7c5db8bbefbd41615c2c12eb
tuning

diff -r 628c97d39627 -r 69e4a4fffea9 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Mar 29 09:45:54 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Mar 29 09:49:39 2016 +0200
@@ -460,7 +460,7 @@
   \label{ssec:datatype-command-syntax}\<close>
 
 subsubsection \<open>\keyw{datatype}
-  \label{sssec:datatype-new}\<close>
+  \label{sssec:datatype}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -1569,7 +1569,7 @@
   \label{ssec:primrec-command-syntax}\<close>
 
 subsubsection \<open>\keyw{primrec}
-  \label{sssec:primrec-new}\<close>
+  \label{sssec:primrec}\<close>
 
 text \<open>
 \begin{matharray}{rcl}