src/HOL/Extraction.thy
changeset 48891 c0eafbd55de3
parent 37233 b78f31ca4675
child 52486 b1565e37678b
--- 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 {*