--- a/src/HOL/Extraction.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Extraction.thy Wed Feb 12 08:35:56 2014 +0100
@@ -5,7 +5,7 @@
header {* Program extraction for HOL *}
theory Extraction
-imports Option
+imports Datatype Option
begin
ML_file "Tools/rewrite_hol_proof.ML"