| changeset 58121 | d7550665da31 |
| parent 58107 | f3c5360711e9 |
| child 58151 | 414deb2ef328 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 01 16:17:47 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 01 16:17:47 2014 +0200 @@ -598,7 +598,7 @@ text {* \blankline *} - ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} + ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *} text {* The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.