# HG changeset patch # User blanchet # Date 1314192339 -7200 # Node ID c471a2b48fa13517df2a48a4f6511491b87449b7 # Parent d9a657c443802a43434ad602b6a30163ade04db7 make sure that all facts are passed to ATP from minimizer diff -r d9a657c44380 -r c471a2b48fa1 src/HOL/Tools/ATP/atp_translate.ML --- 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 **) diff -r d9a657c44380 -r c471a2b48fa1 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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}