--- a/src/HOL/Tools/recdef_package.ML Wed Apr 13 18:45:09 2005 +0200 +++ b/src/HOL/Tools/recdef_package.ML Wed Apr 13 18:45:25 2005 +0200 @@ -382,3 +382,4 @@ end; +