1.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -4,10 +4,11 @@
     1.4  
     1.5  theory Mirabelle
     1.6  imports Sledgehammer
     1.7 -uses "Tools/mirabelle.ML"
     1.8 -     "../TPTP/sledgehammer_tactics.ML"
     1.9  begin
    1.10  
    1.11 +ML_file "Tools/mirabelle.ML"
    1.12 +ML_file "../TPTP/sledgehammer_tactics.ML"
    1.13 +
    1.14  (* no multithreading, no parallel proofs *)  (* FIXME *)
    1.15  ML {* Multithreading.max_threads := 1 *}
    1.16  ML {* Goal.parallel_proofs := 0 *}