--- a/src/HOL/Extraction.thy Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Extraction.thy Wed Mar 04 10:47:20 2009 +0100
@@ -6,7 +6,7 @@
header {* Program extraction for HOL *}
theory Extraction
-imports Datatype
+imports Option
uses "Tools/rewrite_hol_proof.ML"
begin