diff -r cc47e252b92c -r 04f2d3c510d0 src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Sun Mar 04 00:27:07 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: HOL/Import/import_syntax.ML - Author: Sebastian Skalberg (TU Muenchen) -*) - -signature IMPORTER_IMPORT_SYNTAX = -sig -end - -structure Importer_Import_Syntax : IMPORTER_IMPORT_SYNTAX = -struct - -end