1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Dec 06 11:26:17 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Dec 06 11:41:24 2010 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4      val problem =
     1.5        {state = st', goal = goal, subgoal = i,
     1.6         subgoal_count = Sledgehammer_Util.subgoal_count st,
     1.7 -       facts = facts |> map Sledgehammer.Untranslated, only = true}
     1.8 +       facts = facts |> map Sledgehammer.Untranslated}
     1.9      val time_limit =
    1.10        (case hard_timeout of
    1.11          NONE => I

     2.1 --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Dec 06 11:26:17 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Dec 06 11:41:24 2010 +0100
     2.3 @@ -43,8 +43,7 @@
     2.4                          (prop_of goal))
     2.5      val problem =
     2.6        {state = Proof.init ctxt, goal = goal, subgoal = i,
     2.7 -       facts = map Sledgehammer.Untranslated facts,
     2.8 -       only = true, subgoal_count = n}
     2.9 +       subgoal_count = n, facts = map Sledgehammer.Untranslated facts}
    2.10    in
    2.11      (case prover params (K "") problem of
    2.12        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 11:26:17 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 11:41:24 2010 +0100
     3.3 @@ -39,8 +39,7 @@
     3.4       goal: thm,
     3.5       subgoal: int,
     3.6       subgoal_count: int,
     3.7 -     facts: fact list,
     3.8 -     only: bool}
     3.9 +     facts: fact list}
    3.10  
    3.11    type prover_result =
    3.12      {outcome: failure option,
    3.13 @@ -224,8 +223,7 @@
    3.14     goal: thm,
    3.15     subgoal: int,
    3.16     subgoal_count: int,
    3.17 -   facts: fact list,
    3.18 -   only: bool}
    3.19 +   facts: fact list}
    3.20  
    3.21  type prover_result =
    3.22    {outcome: failure option,
    3.23 @@ -287,18 +285,15 @@
    3.24  
    3.25  fun run_atp auto atp_name
    3.26          {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
    3.27 -         known_failures, default_max_relevant, explicit_forall,
    3.28 -         use_conjecture_for_hypotheses}
    3.29 -        ({debug, verbose, overlord, full_types, explicit_apply,
    3.30 -          max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
    3.31 -        minimize_command
    3.32 -        ({state, goal, subgoal, facts, only, ...} : prover_problem) =
    3.33 +         known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
    3.34 +        ({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
    3.35 +          isar_shrink_factor, timeout, ...} : params)
    3.36 +        minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    3.37    let
    3.38      val ctxt = Proof.context_of state
    3.39      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    3.40      val facts =
    3.41 -      facts |> not only ? take (the_default default_max_relevant max_relevant)
    3.42 -            |> map (translated_fact ctxt)
    3.43 +      facts |> map (translated_fact ctxt)
    3.44      val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    3.45                     else Config.get ctxt dest_dir
    3.46      val problem_prefix = Config.get ctxt problem_prefix
    3.47 @@ -538,9 +533,8 @@
    3.48              (Config.put Metis_Tactics.verbose debug
    3.49               #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
    3.50  
    3.51 -fun run_smt_solver auto name (params as {debug, max_relevant, ...})
    3.52 -        minimize_command
    3.53 -        ({state, subgoal, subgoal_count, facts, only, ...} : prover_problem) =
    3.54 +fun run_smt_solver auto name (params as {debug, ...}) minimize_command
    3.55 +        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
    3.56    let
    3.57      val (remote, suffix) =
    3.58        case try (unprefix remote_prefix) name of
    3.59 @@ -551,13 +545,9 @@
    3.60        #> Config.put SMT_Config.verbose debug
    3.61        #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
    3.62      val state = state |> Proof.map_context repair_context
    3.63 -    val ctxt = Proof.context_of state
    3.64      val thy = Proof.theory_of state
    3.65      val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
    3.66 -    val default_max_relevant = SMT_Solver.default_max_relevant ctxt suffix
    3.67 -    val facts =
    3.68 -      facts |> map_filter get_fact
    3.69 -            |> not only ? take (the_default default_max_relevant max_relevant)
    3.70 +    val facts = facts |> map_filter get_fact
    3.71      val {outcome, used_facts, run_time_in_msecs} =
    3.72        smt_filter_loop params remote state subgoal facts
    3.73      val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
    3.74 @@ -595,19 +585,21 @@
    3.75    end
    3.76  
    3.77  fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
    3.78 -               auto minimize_command
    3.79 -               (problem as {state, goal, subgoal, subgoal_count, facts, ...})
    3.80 -               name =
    3.81 +               auto minimize_command only
    3.82 +               {state, goal, subgoal, subgoal_count, facts} name =
    3.83    let
    3.84      val ctxt = Proof.context_of state
    3.85      val birth_time = Time.now ()
    3.86      val death_time = Time.+ (birth_time, timeout)
    3.87      val max_relevant =
    3.88        the_default (default_max_relevant_for_prover ctxt name) max_relevant
    3.89 -    val num_facts = Int.min (length facts, max_relevant)
    3.90 +    val num_facts = length facts |> not only ? Integer.min max_relevant
    3.91      val desc =
    3.92        prover_description ctxt params name num_facts subgoal subgoal_count goal
    3.93      val prover = get_prover ctxt auto name
    3.94 +    val problem =
    3.95 +      {state = state, goal = goal, subgoal = subgoal,
    3.96 +       subgoal_count = subgoal_count, facts = take num_facts facts}
    3.97      fun go () =
    3.98        let
    3.99          fun really_go () =
   3.100 @@ -694,8 +686,8 @@
   3.101                |> map maybe_translate
   3.102              val problem =
   3.103                {state = state, goal = goal, subgoal = i, subgoal_count = n,
   3.104 -               facts = facts, only = only}
   3.105 -            val run_prover = run_prover params auto minimize_command
   3.106 +               facts = facts}
   3.107 +            val run_prover = run_prover params auto minimize_command only
   3.108            in
   3.109              if debug then
   3.110                Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Dec 06 11:26:17 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Dec 06 11:41:24 2010 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4      val {goal, ...} = Proof.goal state
     4.5      val problem =
     4.6        {state = state, goal = goal, subgoal = i, subgoal_count = n,
     4.7 -       facts = facts, only = true}
     4.8 +       facts = facts}
     4.9      val result as {outcome, used_facts, ...} = prover params (K "") problem
    4.10    in
    4.11      Output.urgent_message