--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 14:09:45 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 14:10:40 2010 +0100
@@ -254,7 +254,8 @@
val facts = get_facts "SMT solver" true smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact thy
fun smt_head facts =
- try (SMT_Solver.smt_filter_head state (facts ()))
+ (if debug then curry (op o) SOME else try)
+ (SMT_Solver.smt_filter_head state (facts ()))
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)