--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 11:17:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 15:25:39 2011 +0200
@@ -1062,11 +1062,10 @@
fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
| s_not_trueprop t = s_not t
-fun make_conjecture thy format type_enc ps =
- map2 (fn j => fn ((name, loc), (kind, t)) =>
- t |> kind = Conjecture ? s_not_trueprop
- |> make_formula thy type_enc (format <> CNF) name loc kind)
- (0 upto length ps - 1) ps
+fun make_conjecture thy format type_enc =
+ map (fn ((name, loc), (kind, t)) =>
+ t |> kind = Conjecture ? s_not_trueprop
+ |> make_formula thy type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 11:17:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 15:25:39 2011 +0200
@@ -57,16 +57,16 @@
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
else "") ^ "...")
val {goal, ...} = Proof.goal state
+ val facts =
+ facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, sound = true,
- relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+ relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = false,
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
- val facts =
- facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}