--- 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 ATP
+imports Record
keywords "smt_status" :: diag
begin