# HG changeset patch
# User haftmann
# Date 1257865897 -3600
# Node ID ef54e2108b74a99047c15d2d24663ea835d51886
# Parent  a4dbf0f92d9644eaafff43eb12a7012d79e0a16d
tuned imports

diff -r a4dbf0f92d96 -r ef54e2108b74 src/HOL/ATP_Linkup.thy
--- 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"
diff -r a4dbf0f92d96 -r ef54e2108b74 src/HOL/List.thy
--- 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
 
diff -r a4dbf0f92d96 -r ef54e2108b74 src/HOL/Plain.thy
--- 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 {*
diff -r a4dbf0f92d96 -r ef54e2108b74 src/HOL/Refute.thy
--- 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"