--- a/src/HOL/Plain.thy Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Plain.thy Fri Feb 06 13:43:19 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record SAT Extraction Divides
+imports Datatype FunDef Record Extraction Divides
begin
text {*