author | blanchet |
Mon, 01 Sep 2014 16:17:47 +0200 | |
changeset 58121 | d7550665da31 |
parent 58120 | a14b8d77b15a |
child 58122 | eaac3e01158a |
--- 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}.