--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
@@ -493,6 +493,7 @@
fun pconsts_in_fact thy is_built_in_const t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
(pconsts_in_terms thy is_built_in_const true (SOME true) [t]) []
+
fun pair_consts_fact thy is_built_in_const fudge fact =
case fact |> snd |> theory_const_prop_of fudge
|> pconsts_in_fact thy is_built_in_const of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
@@ -328,7 +328,7 @@
fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
fun atp_translated_fact ctxt fact =
- translate_atp_fact ctxt false (untranslated_fact fact)
+ translate_atp_fact ctxt false (untranslated_fact fact)
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
| smt_weighted_fact ctxt num_facts (fact, j) =
(untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts