--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
@@ -183,14 +183,14 @@
val state =
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
- val {facts = chained_ths, goal, ...} = Proof.goal state
+ val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css_table
- chained_ths hyp_ts concl_t
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+ concl_t
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")