src/HOL/Refute.thy

--- a/src/HOL/Refute.thy	Wed Apr 02 15:58:43 2008 +0200
+++ b/src/HOL/Refute.thy	Wed Apr 02 15:58:57 2008 +0200
@@ -9,11 +9,12 @@
 header {* Refute *}
 
 theory Refute
-imports Datatype
-uses "Tools/prop_logic.ML"
-     "Tools/sat_solver.ML"
-     "Tools/refute.ML"
-     "Tools/refute_isar.ML"
+imports Inductive
+uses
+  "Tools/prop_logic.ML"
+  "Tools/sat_solver.ML"
+  "Tools/refute.ML"
+  "Tools/refute_isar.ML"
 begin
 
 setup Refute.setup