# 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}.