--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 07 06:58:52 2011 +0200
@@ -130,7 +130,7 @@
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_sys
-> bool option -> bool -> bool -> term list -> term
- -> ((string * locality) * thm) list
+ -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -1386,10 +1386,10 @@
facts =
let
val thy = Proof_Context.theory_of ctxt
- val fact_ts = facts |> map (prop_of o snd)
+ val fact_ts = facts |> map snd
val (facts, fact_names) =
- facts |> map (fn (name, th) =>
- (name, prop_of th)
+ facts |> map (fn (name, t) =>
+ (name, t)
|> make_fact ctxt format type_sys false true true true
|> rpair name)
|> map_filter (try (apfst the))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 06:58:52 2011 +0200
@@ -155,7 +155,7 @@
is_metis_prover orf is_smt_prover ctxt orf
is_atp_installed (Proof_Context.theory_of ctxt)
-fun get_slices num_facts slicing slices =
+fun get_slices slicing slices =
(0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
val metis_default_max_relevant = 20
@@ -166,8 +166,7 @@
metis_default_max_relevant
else if is_atp thy name then
fold (Integer.max o fst o snd o snd o snd)
- (get_slices 16384 (* large number *) slicing
- (#best_slices (get_atp thy name) ctxt)) 0
+ (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
end
@@ -579,8 +578,7 @@
let
(* If slicing is disabled, we expand the last slice to fill the
entire time available. *)
- val actual_slices =
- get_slices (length facts) slicing (best_slices ctxt)
+ val actual_slices = get_slices slicing (best_slices ctxt)
val num_actual_slices = length actual_slices
fun monomorphize_facts facts =
let
@@ -618,6 +616,7 @@
? filter_out (member (op =) blacklist o fst)
|> polymorphism_of_type_sys type_sys <> Polymorphic
? monomorphize_facts
+ |> map (apsnd prop_of )
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
--- a/src/HOL/ex/tptp_export.ML Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Tue Jun 07 06:58:52 2011 +0200
@@ -101,7 +101,7 @@
val facts0 = facts_of thy
val facts =
facts0 |> map (fn ((_, loc), (_, th)) =>
- ((Thm.get_name_hint th, loc), th))
+ ((Thm.get_name_hint th, loc), prop_of th))
val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
ATP_Translate.prepare_atp_problem ctxt format