# 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}