src/HOL/TPTP/sledgehammer_tactics.ML

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -22,7 +22,7 @@
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 open Sledgehammer_MaSh
-open Sledgehammer_Isar
+open Sledgehammer_Commands
 
 fun run_prover override_params fact_override i n ctxt goal =
   let