--- a/src/HOL/ATP_Linkup.thy Mon Nov 09 21:56:55 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Tue Nov 10 16:11:37 2009 +0100
@@ -7,7 +7,7 @@
header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
-imports Divides Record Hilbert_Choice Plain
+imports Plain Hilbert_Choice
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
--- a/src/HOL/List.thy Mon Nov 09 21:56:55 2009 +0100
+++ b/src/HOL/List.thy Tue Nov 10 16:11:37 2009 +0100
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Presburger Recdef ATP_Linkup
+imports Plain Presburger ATP_Linkup Recdef
uses ("Tools/list_code.ML")
begin
--- a/src/HOL/Plain.thy Mon Nov 09 21:56:55 2009 +0100
+++ b/src/HOL/Plain.thy Tue Nov 10 16:11:37 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction
+imports Datatype Record FunDef Extraction
begin
text {*
--- a/src/HOL/Refute.thy Mon Nov 09 21:56:55 2009 +0100
+++ b/src/HOL/Refute.thy Tue Nov 10 16:11:37 2009 +0100
@@ -8,7 +8,7 @@
header {* Refute *}
theory Refute
-imports Hilbert_Choice List Record
+imports Hilbert_Choice List
uses
"Tools/prop_logic.ML"
"Tools/sat_solver.ML"