1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -313,7 +313,7 @@
     1.4        in File.append path s end
     1.5    in List.app do_thm ths end
     1.6  
     1.7 -fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy
     1.8 +fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
     1.9                                include_thy file_name =
    1.10    let
    1.11      val path = file_name |> Path.explode
    1.12 @@ -347,7 +347,7 @@
    1.13                  facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    1.14                val facts =
    1.15                  facts |> iterative_relevant_facts ctxt params (hd provers)
    1.16 -                             (the max_relevant) NONE hyp_ts concl_t
    1.17 +                             (the max_facts) NONE hyp_ts concl_t
    1.18                        |> fold (add_isa_dep facts) isa_deps
    1.19                        |> map fix_name
    1.20              in
    1.21 @@ -378,11 +378,11 @@
    1.22  fun learn_proof thy t ths =
    1.23    ()
    1.24  
    1.25 -fun relevant_facts ctxt params prover max_relevant
    1.26 -        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    1.27 +fun relevant_facts ctxt params prover max_facts
    1.28 +                   ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    1.29    if only then
    1.30      facts
    1.31 -  else if max_relevant <= 0 then
    1.32 +  else if max_facts <= 0 then
    1.33      []
    1.34    else
    1.35      let
    1.36 @@ -390,10 +390,11 @@
    1.37        fun prepend_facts ths accepts =
    1.38          ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
    1.39           (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
    1.40 -        |> take max_relevant
    1.41 +        |> take max_facts
    1.42      in
    1.43 -      iterative_relevant_facts ctxt params prover max_relevant NONE
    1.44 -                               hyp_ts concl_t facts
    1.45 +      facts
    1.46 +      |> iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
    1.47 +                                  concl_t
    1.48        |> not (null add_ths) ? prepend_facts add_ths
    1.49      end
    1.50