--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 08:14:56 2010 +0100
@@ -264,6 +264,8 @@
in
raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
end)
+
+ val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
in
fun add_solver cfg =
@@ -271,7 +273,7 @@
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
reconstruct} = cfg
- fun core_oracle () = @{cprop False}
+ fun core_oracle () = cfalse
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
interface=interface,
@@ -312,6 +314,8 @@
"contains the universal sort {}"))
else solver_of ctxt rm ctxt irules
+val cnot = Thm.cterm_of @{theory} @{const Not}
+
fun smt_filter run_remote time_limit st xrules i =
let
val {facts, goal, ...} = Proof.goal st
@@ -322,10 +326,8 @@
|> Config.put C.drop_bad_facts true
|> Config.put C.filter_only_facts true
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
- val cprop =
- concl
- |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
- |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+ fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+ val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in