# HG changeset patch
# User blanchet
# Date 1384968745 -3600
# Node ID f37354a894a3770ceae38bee016abe93641cac4c
# Parent  69b3ff79a69ecbc72869091ac22fd5e304ae133f
fixed LaTeX missing }

diff -r 69b3ff79a69e -r f37354a894a3 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 20 18:09:23 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 20 18:32:25 2013 +0100
@@ -914,10 +914,10 @@
 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
 to register new-style datatypes as old-style datatypes.
 
-\item \emph{The constants @{text "t_case"} and @{text "t_rec"} are now called
-@{text "case_t"} and @{text "rec_t"}.
-
-\item \emph{The recursor @{text "rec_t"} has a different signature for nested
+\item \emph{The constants @{text t_case} and @{text t_rec} are now called
+@{text case_t} and @{text rec_t}.}
+
+\item \emph{The recursor @{text rec_t} has a different signature for nested
 recursive datatypes.} In the old package, nested recursion through non-functions
 was internally reduced to mutual recursion. This reduction was visible in the
 type of the recursor, used by \keyw{primrec}. Recursion through functions was