--- a/src/HOL/ATP.thy Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/ATP.thy Wed Jul 30 14:03:13 2014 +0200
@@ -6,7 +6,7 @@
header {* Automatic Theorem Provers (ATPs) *}
theory ATP
-imports Meson Hilbert_Choice
+imports Meson
begin
subsection {* ATP problems and proofs *}