--- a/src/HOL/Tools/SMT/cvc3_solver.ML Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/Tools/SMT/cvc3_solver.ML Wed May 12 23:54:04 2010 +0200
@@ -35,7 +35,7 @@
else raise SMT_Solver.SMT (solver_name ^ " failed")
end
-fun smtlib_solver oracle _ = {
+fun solver oracle _ = {
command = {env_var=env_var, remote_name=SOME solver_name},
arguments = options,
interface = SMTLIB_Interface.interface,
@@ -43,6 +43,6 @@
val setup =
Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
- SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
+ Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
end