--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 21:44:36 2012 +0200
@@ -41,9 +41,6 @@
(*tactic*)
val smt_tac: Proof.context -> thm list -> int -> tactic
val smt_tac': Proof.context -> thm list -> int -> tactic
-
- (*setup*)
- val setup: theory -> theory
end
structure SMT_Solver: SMT_SOLVER =
@@ -373,17 +370,4 @@
end
-
-val smt_method =
- Scan.optional Attrib.thms [] >>
- (fn thms => fn ctxt => METHOD (fn facts =>
- HEADGOAL (smt_tac ctxt (thms @ facts))))
-
-
-(* setup *)
-
-val setup =
- Method.setup @{binding smt} smt_method
- "Applies an SMT solver to the current goal."
-
end