src/HOL/Extraction.thy

--- a/src/HOL/Extraction.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Extraction.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,9 +5,10 @@
 
 header {* Program extraction for HOL *}
 
-theory Extraction = Datatype
-files
-  "Tools/rewrite_hol_proof.ML":
+theory Extraction
+import Datatype
+files "Tools/rewrite_hol_proof.ML"
+begin
 
 subsection {* Setup *}