--- a/src/HOL/Refute.thy Mon Nov 13 15:43:08 2006 +0100
+++ b/src/HOL/Refute.thy Mon Nov 13 15:43:09 2006 +0100
@@ -9,7 +9,7 @@
header {* Refute *}
theory Refute
-imports Map
+imports Datatype
uses "Tools/prop_logic.ML"
"Tools/sat_solver.ML"
"Tools/refute.ML"