# HG changeset patch
# User blanchet
# Date 1292850585 -3600
# Node ID 7f6baec2b27a724f0beef3d87adf093be19b5f13
# Parent  2dc1dfc1bc698bfc3a21712f81ba3b50dedfb201
remove spurious line

diff -r 2dc1dfc1bc69 -r 7f6baec2b27a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 13:52:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 14:09:45 2010 +0100
@@ -360,7 +360,6 @@
         error ("No such directory: " ^ quote dest_dir ^ ".")
     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
-val command = Path.explode ("/Users/blanchet/misc/E-weights/PROVER/" ^ snd exec) (*###*)
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");