--- a/src/HOL/Refute.thy Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Refute.thy Fri Feb 06 13:43:19 2009 +0100
@@ -9,7 +9,7 @@
header {* Refute *}
theory Refute
-imports Inductive
+imports Hilbert_Choice List Record
uses
"Tools/prop_logic.ML"
"Tools/sat_solver.ML"