# HG changeset patch # User blanchet # Date 1409581067 -7200 # Node ID d7550665da316cbca51db78fa5bdf22823a0f5b8 # Parent a14b8d77b15aed2a7e0c2722f15f6ed57279e04a compile diff -r a14b8d77b15a -r d7550665da31 src/Doc/Datatypes/Datatypes.thy --- 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}.