diff -r e8c5e95d338b -r dd511ddcb203 src/HOL/Library/Refute.thy
--- a/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -8,7 +8,7 @@
 header {* Refute *}
 
 theory Refute
-imports Hilbert_Choice List Sledgehammer
+imports Main
 keywords "refute" :: diag and "refute_params" :: thy_decl
 begin