--- a/src/HOL/Plain.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Plain.thy Wed Oct 28 19:09:47 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides
+imports Datatype FunDef Record Extraction
begin
text {*