--- a/src/HOL/Extraction.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Extraction.thy Wed Aug 22 22:55:41 2012 +0200
@@ -6,9 +6,10 @@
theory Extraction
imports Option
-uses "Tools/rewrite_hol_proof.ML"
begin
+ML_file "Tools/rewrite_hol_proof.ML"
+
subsection {* Setup *}
setup {*