src/HOL/Reconstruction.thy
changeset 20809 6c4fd0b4b63a
parent 20788 d51711512d07
child 20862 1059f2316f88
--- a/src/HOL/Reconstruction.thy	Sun Oct 01 18:29:25 2006 +0200
+++ b/src/HOL/Reconstruction.thy	Sun Oct 01 18:29:26 2006 +0200
@@ -7,7 +7,7 @@
 header{* Reconstructing external resolution proofs *}
 
 theory Reconstruction
-imports Hilbert_Choice Map Infinite_Set Extraction
+imports Hilbert_Choice Map Extraction
 uses 	 "Tools/polyhash.ML"
 	 "Tools/ATP/AtpCommunication.ML"
 	 "Tools/ATP/watcher.ML"