src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 41315 7f6baec2b27a
parent 41313 a96ac4d180b7
child 41318 adcb92c0513b
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 13:52:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 14:09:45 2010 +0100
     1.3 @@ -360,7 +360,6 @@
     1.4          error ("No such directory: " ^ quote dest_dir ^ ".")
     1.5      val measure_run_time = verbose orelse Config.get ctxt measure_run_time
     1.6      val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     1.7 -val command = Path.explode ("/Users/blanchet/misc/E-weights/PROVER/" ^ snd exec) (*###*)
     1.8      fun split_time s =
     1.9        let
    1.10          val split = String.tokens (fn c => str c = "\n");