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