--- a/src/HOL/Sledgehammer.thy Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Aug 28 00:40:38 2014 +0200
@@ -7,7 +7,7 @@
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports Presburger SMT2
+imports Presburger SMT
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
begin
@@ -26,7 +26,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"