src/HOL/TPTP/MaSh_Eval.thy

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,9 +6,10 @@
 
 theory MaSh_Eval
 imports Complex_Main
-uses "mash_eval.ML"
 begin
 
+ML_file "mash_eval.ML"
+
 sledgehammer_params
   [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
    lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]