--- a/src/HOL/Refute.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Refute.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -10,9 +10,9 @@
 theory Refute
 imports Hilbert_Choice List Sledgehammer
 keywords "refute" :: diag and "refute_params" :: thy_decl
-uses "Tools/refute.ML"
 begin
 
+ML_file "Tools/refute.ML"
 setup Refute.setup
 
 refute_params