diff -r e904580c3ee0 -r e50f95ccde99 src/Pure/Tools/codegen_package.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/codegen_package.ML	Sun Aug 28 10:05:03 2005 +0200
@@ -0,0 +1,8 @@
+signature CODEGEN_PACKAGE =
+sig
+end;
+
+structure CodegenPackage : CODEGEN_PACKAGE =
+struct
+
+end;