fixed LaTeX missing }
Wed, 20 Nov 2013 18:32:25 +0100
changeset 54537 f37354a894a3
parent 54536 69b3ff79a69e
child 54538 ba7392b52a7c
fixed LaTeX missing }
--- 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