diff -r d52012eabf0d -r 489083abce44 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
 
 theory SMT
-imports List
+imports ATP
 keywords "smt_status" :: diag
 begin