--- a/src/HOL/Import/HOL4Setup.thy Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/HOL4Setup.thy Wed Feb 15 23:57:06 2006 +0100
@@ -3,9 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Setup imports MakeEqual
- uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
- ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
+theory HOL4Setup imports MakeEqual ImportRecorder
+ uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
section {* General Setup *}