src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 40181 3788b7adab36
parent 40144 23adc2138704
child 40341 03156257040f
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 13:16:43 2010 +0200
@@ -130,9 +130,6 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-(* FIXME: dummy *)
-fun is_smt_solver_installed ctxt = true
-
 fun remotify_prover_if_available_and_not_already_remote thy name =
   if String.isPrefix remote_prefix name then
     SOME name