# HG changeset patch
# User wenzelm
# Date 1113410709 -7200
# Node ID 93163972dbdcfb0fa1e650885c9e1e898269d6d8
# Parent  727ef1b8b3ee8863d9f141643f55fc75bd64915c
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
Args.maybe;

diff -r 727ef1b8b3ee -r 93163972dbdc src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Apr 13 18:34:22 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 13 18:45:09 2005 +0200
@@ -1012,3 +1012,4 @@
 
 structure BasicDatatypePackage: BASIC_DATATYPE_PACKAGE = DatatypePackage;
 open BasicDatatypePackage;
+