--- a/src/HOL/Extraction.thy Sat Oct 12 15:41:59 2019 +0200
+++ b/src/HOL/Extraction.thy Sat Oct 12 16:46:33 2019 +0200
@@ -8,8 +8,6 @@
imports Option
begin
-ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
-
subsection \<open>Setup\<close>
setup \<open>