--- a/src/HOL/List.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/List.thy Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
+imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
begin
datatype_new (set: 'a) list =
--- a/src/HOL/Nitpick.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Nitpick.thy Thu Jun 12 01:00:49 2014 +0200
@@ -8,7 +8,7 @@
header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
theory Nitpick
-imports BNF_FP_Base Map Record Sledgehammer
+imports BNF_FP_Base Map Record
keywords
"nitpick" :: diag and
"nitpick_params" :: thy_decl
--- 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
--- a/src/HOL/Sledgehammer.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Jun 12 01:00:49 2014 +0200
@@ -7,7 +7,7 @@
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports ATP SMT2
+imports Presburger ATP SMT2
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
begin