src/HOL/IsaMakefile
changeset 43918 6ca79a354c51
parent 43917 bce3de79c8ce
child 43925 f651cb053927
--- a/src/HOL/IsaMakefile	Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 20 10:11:08 2011 +0200
@@ -555,13 +555,11 @@
 ## HOL-Import
 
 IMPORTER_FILES = \
-  Import/ImportRecorder.thy Import/HOL4Compat.thy \
+  Import/HOL4Compat.thy \
   Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \
   Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \
-  Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \
-  Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \
-  Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \
-  Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \
+  Import/import.ML Import/import_syntax.ML \
+  Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \
   Library/ContNotDenum.thy Old_Number_Theory/Primes.thy
 
 HOL-Import: HOL $(LOG)/HOL-Import.gz