standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
authorblanchet
Tue Oct 26 21:01:28 2010 +0200 (2010-10-26)
changeset 40204da97d75e20e6
parent 40203 aff7d1471b62
child 40205 277508b07418
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 20:12:33 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 21:01:28 2010 +0200
     1.3 @@ -357,25 +357,25 @@
     1.4      val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
     1.5      val relevance_override = {add = [], del = [], only = false}
     1.6      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     1.7 -    val axioms =
     1.8 +    val facts =
     1.9        Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
    1.10            (the_default default_max_relevant max_relevant) irrelevant_consts
    1.11            relevance_fudge relevance_override chained_ths hyp_ts concl_t
    1.12      val problem =
    1.13        {state = st', goal = goal, subgoal = i,
    1.14         subgoal_count = Sledgehammer_Util.subgoal_count st,
    1.15 -       axioms = axioms |> map Sledgehammer.Untranslated, only = true}
    1.16 +       facts = facts |> map Sledgehammer.Untranslated, only = true}
    1.17      val time_limit =
    1.18        (case hard_timeout of
    1.19          NONE => I
    1.20        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
    1.21 -    val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...}
    1.22 +    val ({outcome, message, used_facts, run_time_in_msecs = SOME time_prover, ...}
    1.23           : Sledgehammer.prover_result,
    1.24          time_isa) = time_limit (Mirabelle.cpu_time
    1.25                        (prover params (K ""))) problem
    1.26    in
    1.27      case outcome of
    1.28 -      NONE => (message, SH_OK (time_isa, time_prover, used_axioms))
    1.29 +      NONE => (message, SH_OK (time_isa, time_prover, used_facts))
    1.30      | SOME _ => (message, SH_FAIL (time_isa, time_prover))
    1.31    end
    1.32    handle ERROR msg => ("error: " ^ msg, SH_ERROR)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 20:12:33 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:01:28 2010 +0200
     2.3 @@ -30,7 +30,7 @@
     2.4       timeout: Time.time,
     2.5       expect: string}
     2.6  
     2.7 -  datatype axiom =
     2.8 +  datatype fact =
     2.9      Untranslated of (string * locality) * thm |
    2.10      Translated of term * ((string * locality) * translated_formula) option
    2.11  
    2.12 @@ -39,12 +39,12 @@
    2.13       goal: thm,
    2.14       subgoal: int,
    2.15       subgoal_count: int,
    2.16 -     axioms: axiom list,
    2.17 +     facts: fact list,
    2.18       only: bool}
    2.19  
    2.20    type prover_result =
    2.21      {outcome: failure option,
    2.22 -     used_axioms: (string * locality) list,
    2.23 +     used_facts: (string * locality) list,
    2.24       run_time_in_msecs: int option,
    2.25       message: string}
    2.26  
    2.27 @@ -194,7 +194,7 @@
    2.28     timeout: Time.time,
    2.29     expect: string}
    2.30  
    2.31 -datatype axiom =
    2.32 +datatype fact =
    2.33    Untranslated of (string * locality) * thm |
    2.34    Translated of term * ((string * locality) * translated_formula) option
    2.35  
    2.36 @@ -203,13 +203,13 @@
    2.37     goal: thm,
    2.38     subgoal: int,
    2.39     subgoal_count: int,
    2.40 -   axioms: axiom list,
    2.41 +   facts: fact list,
    2.42     only: bool}
    2.43  
    2.44  type prover_result =
    2.45    {outcome: failure option,
    2.46     message: string,
    2.47 -   used_axioms: (string * locality) list,
    2.48 +   used_facts: (string * locality) list,
    2.49     run_time_in_msecs: int option}
    2.50  
    2.51  type prover = params -> minimize_command -> prover_problem -> prover_result
    2.52 @@ -232,11 +232,11 @@
    2.53    |> Exn.release
    2.54    |> tap (after path)
    2.55  
    2.56 -fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
    2.57 -                       i n goal =
    2.58 +fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
    2.59 +                       n goal =
    2.60    quote name ^
    2.61    (if verbose then
    2.62 -     " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
    2.63 +     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    2.64     else
    2.65       "") ^
    2.66    " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
    2.67 @@ -252,8 +252,8 @@
    2.68  
    2.69  fun dest_Untranslated (Untranslated p) = p
    2.70    | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
    2.71 -fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p
    2.72 -  | translated_axiom _ (Translated p) = p
    2.73 +fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
    2.74 +  | translated_fact _ (Translated p) = p
    2.75  
    2.76  fun int_option_add (SOME m) (SOME n) = SOME (m + n)
    2.77    | int_option_add _ _ = NONE
    2.78 @@ -269,13 +269,13 @@
    2.79          ({debug, verbose, overlord, full_types, explicit_apply,
    2.80            max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
    2.81          minimize_command
    2.82 -        ({state, goal, subgoal, axioms, only, ...} : prover_problem) =
    2.83 +        ({state, goal, subgoal, facts, only, ...} : prover_problem) =
    2.84    let
    2.85      val ctxt = Proof.context_of state
    2.86      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    2.87 -    val axioms =
    2.88 -      axioms |> not only ? take (the_default default_max_relevant max_relevant)
    2.89 -             |> map (translated_axiom ctxt)
    2.90 +    val facts =
    2.91 +      facts |> not only ? take (the_default default_max_relevant max_relevant)
    2.92 +            |> map (translated_fact ctxt)
    2.93      val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.94                     else Config.get ctxt dest_dir
    2.95      val problem_prefix = Config.get ctxt problem_prefix
    2.96 @@ -334,9 +334,9 @@
    2.97                        proof_delims known_failures output
    2.98                in (output, msecs, tstplike_proof, outcome) end
    2.99              val readable_names = debug andalso overlord
   2.100 -            val (atp_problem, pool, conjecture_offset, axiom_names) =
   2.101 +            val (atp_problem, pool, conjecture_offset, fact_names) =
   2.102                prepare_atp_problem ctxt readable_names explicit_forall full_types
   2.103 -                                  explicit_apply hyp_ts concl_t axioms
   2.104 +                                  explicit_apply hyp_ts concl_t facts
   2.105              val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   2.106                                                    atp_problem
   2.107              val _ = File.write_list probfile ss
   2.108 @@ -358,7 +358,7 @@
   2.109                                (output, int_option_add msecs0 msecs,
   2.110                                 tstplike_proof, outcome))
   2.111                       | result => result)
   2.112 -          in ((pool, conjecture_shape, axiom_names), result) end
   2.113 +          in ((pool, conjecture_shape, fact_names), result) end
   2.114          else
   2.115            error ("Bad executable: " ^ Path.implode command ^ ".")
   2.116  
   2.117 @@ -371,24 +371,23 @@
   2.118          ()
   2.119        else
   2.120          File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   2.121 -    val ((pool, conjecture_shape, axiom_names),
   2.122 +    val ((pool, conjecture_shape, fact_names),
   2.123           (output, msecs, tstplike_proof, outcome)) =
   2.124        with_path cleanup export run_on problem_path_name
   2.125 -    val (conjecture_shape, axiom_names) =
   2.126 -      repair_conjecture_shape_and_axiom_names output conjecture_shape
   2.127 -                                              axiom_names
   2.128 +    val (conjecture_shape, fact_names) =
   2.129 +      repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
   2.130      val important_message =
   2.131        if random () <= important_message_keep_factor then
   2.132          extract_important_message output
   2.133        else
   2.134          ""
   2.135 -    val (message, used_axioms) =
   2.136 +    val (message, used_facts) =
   2.137        case outcome of
   2.138          NONE =>
   2.139          proof_text isar_proof
   2.140              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   2.141              (proof_banner auto, full_types, minimize_command, tstplike_proof,
   2.142 -             axiom_names, goal, subgoal)
   2.143 +             fact_names, goal, subgoal)
   2.144          |>> (fn message =>
   2.145                  message ^ (if verbose then
   2.146                               "\nATP real CPU time: " ^
   2.147 @@ -402,7 +401,7 @@
   2.148                     ""))
   2.149        | SOME failure => (string_for_failure failure, [])
   2.150    in
   2.151 -    {outcome = outcome, message = message, used_axioms = used_axioms,
   2.152 +    {outcome = outcome, message = message, used_facts = used_facts,
   2.153       run_time_in_msecs = msecs}
   2.154    end
   2.155  
   2.156 @@ -411,12 +410,12 @@
   2.157    | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
   2.158  
   2.159  fun run_smt_solver remote ({timeout, ...} : params) minimize_command
   2.160 -                   ({state, subgoal, subgoal_count, axioms, ...}
   2.161 +                   ({state, subgoal, subgoal_count, facts, ...}
   2.162                      : prover_problem) =
   2.163    let
   2.164      val {outcome, used_facts, run_time_in_msecs} =
   2.165        SMT_Solver.smt_filter remote timeout state
   2.166 -                            (map_filter (try dest_Untranslated) axioms) subgoal
   2.167 +                            (map_filter (try dest_Untranslated) facts) subgoal
   2.168      val message =
   2.169        case outcome of
   2.170          NONE =>
   2.171 @@ -426,11 +425,11 @@
   2.172          minimize_line minimize_command (map fst used_facts)
   2.173        | SOME SMT_Solver.Time_Out => "Timed out."
   2.174        | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
   2.175 -      | SOME (failure as SMT_Solver.Other_Failure message) => message
   2.176 +      | SOME (SMT_Solver.Other_Failure message) => message
   2.177      val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   2.178    in
   2.179 -    {outcome = outcome, used_axioms = used_facts,
   2.180 -     run_time_in_msecs = SOME run_time_in_msecs, message = message}
   2.181 +    {outcome = outcome, used_facts = used_facts,
   2.182 +     run_time_in_msecs = run_time_in_msecs, message = message}
   2.183    end
   2.184  
   2.185  fun get_prover thy auto name =
   2.186 @@ -439,7 +438,7 @@
   2.187  
   2.188  fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
   2.189                 auto minimize_command
   2.190 -               (problem as {state, goal, subgoal, subgoal_count, axioms, ...})
   2.191 +               (problem as {state, goal, subgoal, subgoal_count, facts, ...})
   2.192                 name =
   2.193    let
   2.194      val thy = Proof.theory_of state
   2.195 @@ -448,9 +447,9 @@
   2.196      val death_time = Time.+ (birth_time, timeout)
   2.197      val max_relevant =
   2.198        the_default (default_max_relevant_for_prover thy name) max_relevant
   2.199 -    val num_axioms = Int.min (length axioms, max_relevant)
   2.200 +    val num_facts = Int.min (length facts, max_relevant)
   2.201      val desc =
   2.202 -      prover_description ctxt params name num_axioms subgoal subgoal_count goal
   2.203 +      prover_description ctxt params name num_facts subgoal subgoal_count goal
   2.204      fun go () =
   2.205        let
   2.206          fun really_go () =
   2.207 @@ -522,14 +521,14 @@
   2.208                  0 |> fold (Integer.max o default_max_relevant_for_prover thy)
   2.209                            provers
   2.210                    |> auto ? (fn n => n div auto_max_relevant_divisor)
   2.211 -            val axioms =
   2.212 +            val facts =
   2.213                relevant_facts ctxt full_types relevance_thresholds
   2.214                               max_max_relevant irrelevant_consts relevance_fudge
   2.215                               relevance_override chained_ths hyp_ts concl_t
   2.216                |> map maybe_translate
   2.217              val problem =
   2.218                {state = state, goal = goal, subgoal = i, subgoal_count = n,
   2.219 -               axioms = axioms, only = only}
   2.220 +               facts = facts, only = only}
   2.221              val run_prover = run_prover params auto minimize_command
   2.222            in
   2.223              if auto then
   2.224 @@ -543,7 +542,7 @@
   2.225            end
   2.226        val run_atps =
   2.227          run_provers full_types atp_irrelevant_consts atp_relevance_fudge
   2.228 -                    (Translated o translate_axiom ctxt) atps
   2.229 +                    (Translated o translate_fact ctxt) atps
   2.230        val run_smts =
   2.231          run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
   2.232                      smts
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue Oct 26 20:12:33 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue Oct 26 21:01:28 2010 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4      string Symtab.table * bool * int * Proof.context * int list list
     3.5    type text_result = string * (string * locality) list
     3.6  
     3.7 -  val repair_conjecture_shape_and_axiom_names :
     3.8 +  val repair_conjecture_shape_and_fact_names :
     3.9      string -> int list list -> (string * locality) list vector
    3.10      -> int list list * (string * locality) list vector
    3.11    val apply_on_subgoal : int -> int -> string
    3.12 @@ -57,7 +57,7 @@
    3.13  
    3.14  (** SPASS's Flotter hack **)
    3.15  
    3.16 -(* This is a hack required for keeping track of axioms after they have been
    3.17 +(* This is a hack required for keeping track of facts after they have been
    3.18     clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    3.19     part of this hack. *)
    3.20  
    3.21 @@ -84,8 +84,7 @@
    3.22    #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    3.23    #> fst
    3.24  
    3.25 -fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    3.26 -                                            axiom_names =
    3.27 +fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    3.28    if String.isSubstring set_ClauseFormulaRelationN output then
    3.29      let
    3.30        val j0 = hd (hd conjecture_shape)
    3.31 @@ -97,10 +96,9 @@
    3.32          |> map (fn s => find_index (curry (op =) s) seq + 1)
    3.33        fun names_for_number j =
    3.34          j |> AList.lookup (op =) name_map |> these
    3.35 -          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    3.36 +          |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
    3.37            |> map (fn name =>
    3.38 -                     (name, name |> find_first_in_list_vector axiom_names
    3.39 -                                 |> the)
    3.40 +                     (name, name |> find_first_in_list_vector fact_names |> the)
    3.41                       handle Option.Option =>
    3.42                              error ("No such fact: " ^ quote name ^ "."))
    3.43      in
    3.44 @@ -108,7 +106,7 @@
    3.45         seq |> map names_for_number |> Vector.fromList)
    3.46      end
    3.47    else
    3.48 -    (conjecture_shape, axiom_names)
    3.49 +    (conjecture_shape, fact_names)
    3.50  
    3.51  
    3.52  (** Soft-core proof reconstruction: Metis one-liner **)
    3.53 @@ -139,38 +137,37 @@
    3.54        "\nTo minimize the number of lemmas, try this: " ^
    3.55        Markup.markup Markup.sendback command ^ "."
    3.56  
    3.57 -fun resolve_axiom axiom_names ((_, SOME s)) =
    3.58 -    (case strip_prefix_and_unascii axiom_prefix s of
    3.59 -       SOME s' => (case find_first_in_list_vector axiom_names s' of
    3.60 +fun resolve_fact fact_names ((_, SOME s)) =
    3.61 +    (case strip_prefix_and_unascii fact_prefix s of
    3.62 +       SOME s' => (case find_first_in_list_vector fact_names s' of
    3.63                       SOME x => [(s', x)]
    3.64                     | NONE => [])
    3.65       | NONE => [])
    3.66 -  | resolve_axiom axiom_names (num, NONE) =
    3.67 +  | resolve_fact fact_names (num, NONE) =
    3.68      case Int.fromString num of
    3.69        SOME j =>
    3.70 -      if j > 0 andalso j <= Vector.length axiom_names then
    3.71 -        Vector.sub (axiom_names, j - 1)
    3.72 +      if j > 0 andalso j <= Vector.length fact_names then
    3.73 +        Vector.sub (fact_names, j - 1)
    3.74        else
    3.75          []
    3.76      | NONE => []
    3.77  
    3.78 -fun add_fact axiom_names (Inference (name, _, [])) =
    3.79 -    append (resolve_axiom axiom_names name)
    3.80 +fun add_fact fact_names (Inference (name, _, [])) =
    3.81 +    append (resolve_fact fact_names name)
    3.82    | add_fact _ _ = I
    3.83  
    3.84 -fun used_facts_in_tstplike_proof axiom_names =
    3.85 -  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
    3.86 +fun used_facts_in_tstplike_proof fact_names =
    3.87 +  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
    3.88  
    3.89 -fun used_facts axiom_names =
    3.90 -  used_facts_in_tstplike_proof axiom_names
    3.91 +fun used_facts fact_names =
    3.92 +  used_facts_in_tstplike_proof fact_names
    3.93    #> List.partition (curry (op =) Chained o snd)
    3.94    #> pairself (sort_distinct (string_ord o pairself fst))
    3.95  
    3.96  fun metis_proof_text (banner, full_types, minimize_command,
    3.97 -                      tstplike_proof, axiom_names, goal, i) =
    3.98 +                      tstplike_proof, fact_names, goal, i) =
    3.99    let
   3.100 -    val (chained_lemmas, other_lemmas) =
   3.101 -      used_facts axiom_names tstplike_proof
   3.102 +    val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
   3.103      val n = Logic.count_prems (prop_of goal)
   3.104    in
   3.105      (metis_line banner full_types i n (map fst other_lemmas) ^
   3.106 @@ -233,7 +230,7 @@
   3.107                        | NONE => ~1
   3.108    in if k >= 0 then [k] else [] end
   3.109  
   3.110 -fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   3.111 +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
   3.112  fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   3.113  
   3.114  fun raw_label_for_name conjecture_shape name =
   3.115 @@ -491,14 +488,14 @@
   3.116    | replace_dependencies_in_line p (Inference (name, t, deps)) =
   3.117      Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   3.118  
   3.119 -(* Discard axioms; consolidate adjacent lines that prove the same formula, since
   3.120 +(* Discard facts; consolidate adjacent lines that prove the same formula, since
   3.121     they differ only in type information.*)
   3.122  fun add_line _ _ (line as Definition _) lines = line :: lines
   3.123 -  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   3.124 -    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   3.125 +  | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
   3.126 +    (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   3.127         definitions. *)
   3.128 -    if is_axiom axiom_names name then
   3.129 -      (* Axioms are not proof lines. *)
   3.130 +    if is_fact fact_names name then
   3.131 +      (* Facts are not proof lines. *)
   3.132        if is_only_type_information t then
   3.133          map (replace_dependencies_in_line (name, [])) lines
   3.134        (* Is there a repetition? If so, replace later line by earlier one. *)
   3.135 @@ -541,10 +538,10 @@
   3.136  
   3.137  fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   3.138      (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   3.139 -  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   3.140 +  | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
   3.141                       (Inference (name, t, deps)) (j, lines) =
   3.142      (j + 1,
   3.143 -     if is_axiom axiom_names name orelse
   3.144 +     if is_fact fact_names name orelse
   3.145          is_conjecture conjecture_shape name orelse
   3.146          (* the last line must be kept *)
   3.147          j = 0 orelse
   3.148 @@ -580,20 +577,20 @@
   3.149  fun smart_case_split [] facts = ByMetis facts
   3.150    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   3.151  
   3.152 -fun add_fact_from_dependency conjecture_shape axiom_names name =
   3.153 -  if is_axiom axiom_names name then
   3.154 -    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   3.155 +fun add_fact_from_dependency conjecture_shape fact_names name =
   3.156 +  if is_fact fact_names name then
   3.157 +    apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   3.158    else
   3.159      apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   3.160  
   3.161  fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   3.162    | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   3.163      Assume (raw_label_for_name conjecture_shape name, t)
   3.164 -  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   3.165 +  | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   3.166      Have (if j = 1 then [Show] else [],
   3.167            raw_label_for_name conjecture_shape name,
   3.168            fold_rev forall_of (map Var (Term.add_vars t [])) t,
   3.169 -          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   3.170 +          ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   3.171                          deps ([], [])))
   3.172  
   3.173  fun repair_name "$true" = "c_True"
   3.174 @@ -606,8 +603,9 @@
   3.175      else
   3.176        s
   3.177  
   3.178 -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   3.179 -        tstplike_proof conjecture_shape axiom_names params frees =
   3.180 +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   3.181 +        isar_shrink_factor tstplike_proof conjecture_shape fact_names params
   3.182 +        frees =
   3.183    let
   3.184      val lines =
   3.185        tstplike_proof
   3.186 @@ -615,14 +613,14 @@
   3.187        |> nasty_atp_proof pool
   3.188        |> map_term_names_in_atp_proof repair_name
   3.189        |> decode_lines ctxt full_types tfrees
   3.190 -      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   3.191 +      |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
   3.192        |> rpair [] |-> fold_rev add_nontrivial_line
   3.193        |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   3.194 -                                             conjecture_shape axiom_names frees)
   3.195 +                                             conjecture_shape fact_names frees)
   3.196        |> snd
   3.197    in
   3.198      (if null params then [] else [Fix params]) @
   3.199 -    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   3.200 +    map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   3.201           lines
   3.202    end
   3.203  
   3.204 @@ -915,7 +913,7 @@
   3.205  
   3.206  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   3.207                      (other_params as (_, full_types, _, tstplike_proof,
   3.208 -                                      axiom_names, goal, i)) =
   3.209 +                                      fact_names, goal, i)) =
   3.210    let
   3.211      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   3.212      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   3.213 @@ -924,7 +922,7 @@
   3.214      val (one_line_proof, lemma_names) = metis_proof_text other_params
   3.215      fun isar_proof_for () =
   3.216        case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   3.217 -               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   3.218 +               isar_shrink_factor tstplike_proof conjecture_shape fact_names
   3.219                 params frees
   3.220             |> redirect_proof hyp_ts concl_t
   3.221             |> kill_duplicate_assumptions_in_proof
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 20:12:33 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 21:01:28 2010 +0200
     4.3 @@ -11,9 +11,9 @@
     4.4    type 'a problem = 'a ATP_Problem.problem
     4.5    type translated_formula
     4.6  
     4.7 -  val axiom_prefix : string
     4.8 +  val fact_prefix : string
     4.9    val conjecture_prefix : string
    4.10 -  val translate_axiom :
    4.11 +  val translate_fact :
    4.12      Proof.context -> (string * 'a) * thm
    4.13      -> term * ((string * 'a) * translated_formula) option
    4.14    val prepare_atp_problem :
    4.15 @@ -29,7 +29,7 @@
    4.16  open Metis_Translate
    4.17  open Sledgehammer_Util
    4.18  
    4.19 -val axiom_prefix = "ax_"
    4.20 +val fact_prefix = "fact_"
    4.21  val conjecture_prefix = "conj_"
    4.22  val helper_prefix = "help_"
    4.23  val class_rel_clause_prefix = "clrel_";
    4.24 @@ -174,7 +174,7 @@
    4.25        | aux _ = raise Fail "aux"
    4.26    in perhaps (try aux) end
    4.27  
    4.28 -(* making axiom and conjecture formulas *)
    4.29 +(* making fact and conjecture formulas *)
    4.30  fun make_formula ctxt presimp name kind t =
    4.31    let
    4.32      val thy = ProofContext.theory_of ctxt
    4.33 @@ -194,7 +194,7 @@
    4.34       ctypes_sorts = ctypes_sorts}
    4.35    end
    4.36  
    4.37 -fun make_axiom ctxt presimp ((name, loc), th) =
    4.38 +fun make_fact ctxt presimp ((name, loc), th) =
    4.39    case make_formula ctxt presimp name Axiom (prop_of th) of
    4.40      {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
    4.41    | formula => SOME ((name, loc), formula)
    4.42 @@ -232,10 +232,10 @@
    4.43    [optional_helpers, optional_typed_helpers] |> maps (maps fst)
    4.44    |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
    4.45  
    4.46 -fun get_helper_facts ctxt is_FO full_types conjectures axioms =
    4.47 +fun get_helper_facts ctxt is_FO full_types conjectures facts =
    4.48    let
    4.49      val ct =
    4.50 -      fold (fold count_translated_formula) [conjectures, axioms] init_counters
    4.51 +      fold (fold count_translated_formula) [conjectures, facts] init_counters
    4.52      fun is_needed c = the (Symtab.lookup ct c) > 0
    4.53      fun baptize th = ((Thm.get_name_hint th, false), th)
    4.54    in
    4.55 @@ -244,32 +244,32 @@
    4.56       |> maps (fn (ss, ths) =>
    4.57                   if exists is_needed ss then map baptize ths else [])) @
    4.58      (if is_FO then [] else map baptize mandatory_helpers)
    4.59 -    |> map_filter (Option.map snd o make_axiom ctxt false)
    4.60 +    |> map_filter (Option.map snd o make_fact ctxt false)
    4.61    end
    4.62  
    4.63 -fun translate_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
    4.64 +fun translate_fact ctxt (ax as (_, th)) = (prop_of th, make_fact ctxt true ax)
    4.65  
    4.66 -fun translate_formulas ctxt full_types hyp_ts concl_t axioms =
    4.67 +fun translate_formulas ctxt full_types hyp_ts concl_t facts =
    4.68    let
    4.69      val thy = ProofContext.theory_of ctxt
    4.70 -    val (axiom_ts, translated_axioms) = ListPair.unzip axioms
    4.71 -    (* Remove existing axioms from the conjecture, as this can dramatically
    4.72 +    val (fact_ts, translated_facts) = ListPair.unzip facts
    4.73 +    (* Remove existing facts from the conjecture, as this can dramatically
    4.74         boost an ATP's performance (for some reason). *)
    4.75 -    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
    4.76 +    val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
    4.77      val goal_t = Logic.list_implies (hyp_ts, concl_t)
    4.78      val is_FO = Meson.is_fol_term thy goal_t
    4.79      val subs = tfree_classes_of_terms [goal_t]
    4.80 -    val supers = tvar_classes_of_terms axiom_ts
    4.81 -    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
    4.82 -    (* TFrees in the conjecture; TVars in the axioms *)
    4.83 +    val supers = tvar_classes_of_terms fact_ts
    4.84 +    val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
    4.85 +    (* TFrees in the conjecture; TVars in the facts *)
    4.86      val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
    4.87 -    val (axiom_names, axioms) = ListPair.unzip (map_filter I translated_axioms)
    4.88 -    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
    4.89 +    val (fact_names, facts) = ListPair.unzip (map_filter I translated_facts)
    4.90 +    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts
    4.91      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    4.92      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    4.93    in
    4.94 -    (axiom_names |> map single |> Vector.fromList,
    4.95 -     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
    4.96 +    (fact_names |> map single |> Vector.fromList,
    4.97 +     (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses))
    4.98    end
    4.99  
   4.100  fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   4.101 @@ -322,14 +322,14 @@
   4.102        | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   4.103    in aux end
   4.104  
   4.105 -fun formula_for_axiom full_types
   4.106 -                      ({combformula, ctypes_sorts, ...} : translated_formula) =
   4.107 +fun formula_for_fact full_types
   4.108 +                     ({combformula, ctypes_sorts, ...} : translated_formula) =
   4.109    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   4.110                  (type_literals_for_types ctypes_sorts))
   4.111             (formula_for_combformula full_types combformula)
   4.112  
   4.113  fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   4.114 -  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   4.115 +  Fof (prefix ^ ascii_of name, kind, formula_for_fact full_types formula)
   4.116  
   4.117  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   4.118                                                         superclass, ...}) =
   4.119 @@ -497,13 +497,13 @@
   4.120        (const_table_for_problem explicit_apply problem) problem
   4.121  
   4.122  fun prepare_atp_problem ctxt readable_names explicit_forall full_types
   4.123 -                        explicit_apply hyp_ts concl_t axioms =
   4.124 +                        explicit_apply hyp_ts concl_t facts =
   4.125    let
   4.126      val thy = ProofContext.theory_of ctxt
   4.127 -    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   4.128 -                       arity_clauses)) =
   4.129 -      translate_formulas ctxt full_types hyp_ts concl_t axioms
   4.130 -    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   4.131 +    val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
   4.132 +                      arity_clauses)) =
   4.133 +      translate_formulas ctxt full_types hyp_ts concl_t facts
   4.134 +    val fact_lines = map (problem_line_for_fact fact_prefix full_types) facts
   4.135      val helper_lines =
   4.136        map (problem_line_for_fact helper_prefix full_types) helper_facts
   4.137      val conjecture_lines =
   4.138 @@ -515,7 +515,7 @@
   4.139      (* Reordering these might or might not confuse the proof reconstruction
   4.140         code or the SPASS Flotter hack. *)
   4.141      val problem =
   4.142 -      [("Relevant facts", axiom_lines),
   4.143 +      [("Relevant facts", fact_lines),
   4.144         ("Class relationships", class_rel_lines),
   4.145         ("Arity declarations", arity_lines),
   4.146         ("Helper facts", helper_lines),
   4.147 @@ -524,12 +524,12 @@
   4.148        |> repair_problem thy explicit_forall full_types explicit_apply
   4.149      val (problem, pool) = nice_atp_problem readable_names problem
   4.150      val conjecture_offset =
   4.151 -      length axiom_lines + length class_rel_lines + length arity_lines
   4.152 +      length fact_lines + length class_rel_lines + length arity_lines
   4.153        + length helper_lines
   4.154    in
   4.155      (problem,
   4.156       case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   4.157 -     conjecture_offset, axiom_names)
   4.158 +     conjecture_offset, fact_names)
   4.159    end
   4.160  
   4.161  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 26 20:12:33 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 26 21:01:28 2010 +0200
     5.3 @@ -283,7 +283,7 @@
     5.4  
     5.5  structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
     5.6  
     5.7 -fun count_axiom_consts thy fudge =
     5.8 +fun count_fact_consts thy fudge =
     5.9    let
    5.10      fun do_const const (s, T) ts =
    5.11        (* Two-dimensional table update. Constant maps to types maps to count. *)
    5.12 @@ -357,9 +357,9 @@
    5.13    | locality_bonus {assum_bonus, ...} Assum = assum_bonus
    5.14    | locality_bonus {chained_bonus, ...} Chained = chained_bonus
    5.15  
    5.16 -fun axiom_weight fudge loc const_tab relevant_consts axiom_consts =
    5.17 -  case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
    5.18 -                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
    5.19 +fun fact_weight fudge loc const_tab relevant_consts fact_consts =
    5.20 +  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
    5.21 +                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
    5.22      ([], _) => 0.0
    5.23    | (rel, irrel) =>
    5.24      let
    5.25 @@ -372,14 +372,14 @@
    5.26        val res = rel_weight / (rel_weight + irrel_weight)
    5.27      in if Real.isFinite res then res else 0.0 end
    5.28  
    5.29 -fun pconsts_in_axiom thy irrelevant_consts t =
    5.30 +fun pconsts_in_fact thy irrelevant_consts t =
    5.31    Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
    5.32                (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) []
    5.33 -fun pair_consts_axiom thy irrelevant_consts fudge axiom =
    5.34 -  case axiom |> snd |> theory_const_prop_of fudge
    5.35 -             |> pconsts_in_axiom thy irrelevant_consts of
    5.36 +fun pair_consts_fact thy irrelevant_consts fudge fact =
    5.37 +  case fact |> snd |> theory_const_prop_of fudge
    5.38 +            |> pconsts_in_fact thy irrelevant_consts of
    5.39      [] => NONE
    5.40 -  | consts => SOME ((axiom, consts), NONE)
    5.41 +  | consts => SOME ((fact, consts), NONE)
    5.42  
    5.43  type annotated_thm =
    5.44    (((unit -> string) * locality) * thm) * (string * ptype) list
    5.45 @@ -407,27 +407,27 @@
    5.46      (accepts, more_rejects @ rejects)
    5.47    end
    5.48  
    5.49 -fun if_empty_replace_with_locality thy irrelevant_consts axioms loc tab =
    5.50 +fun if_empty_replace_with_locality thy irrelevant_consts facts loc tab =
    5.51    if Symtab.is_empty tab then
    5.52      pconsts_in_terms thy irrelevant_consts false (SOME false)
    5.53          (map_filter (fn ((_, loc'), th) =>
    5.54 -                        if loc' = loc then SOME (prop_of th) else NONE) axioms)
    5.55 +                        if loc' = loc then SOME (prop_of th) else NONE) facts)
    5.56    else
    5.57      tab
    5.58  
    5.59  fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
    5.60          (fudge as {threshold_divisor, ridiculous_threshold, ...})
    5.61 -        ({add, del, ...} : relevance_override) axioms goal_ts =
    5.62 +        ({add, del, ...} : relevance_override) facts goal_ts =
    5.63    let
    5.64      val thy = ProofContext.theory_of ctxt
    5.65 -    val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty
    5.66 +    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
    5.67      val goal_const_tab =
    5.68        pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts
    5.69 -      |> fold (if_empty_replace_with_locality thy irrelevant_consts axioms)
    5.70 +      |> fold (if_empty_replace_with_locality thy irrelevant_consts facts)
    5.71                [Chained, Assum, Local]
    5.72      val add_ths = Attrib.eval_thms ctxt add
    5.73      val del_ths = Attrib.eval_thms ctxt del
    5.74 -    val axioms = axioms |> filter_out (member Thm.eq_thm del_ths o snd)
    5.75 +    val facts = facts |> filter_out (member Thm.eq_thm del_ths o snd)
    5.76      fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
    5.77        let
    5.78          fun relevant [] _ [] =
    5.79 @@ -476,14 +476,14 @@
    5.80                        hopeless_rejects hopeful_rejects)
    5.81              end
    5.82            | relevant candidates rejects
    5.83 -                     (((ax as (((_, loc), _), axiom_consts)), cached_weight)
    5.84 +                     (((ax as (((_, loc), _), fact_consts)), cached_weight)
    5.85                        :: hopeful) =
    5.86              let
    5.87                val weight =
    5.88                  case cached_weight of
    5.89                    SOME w => w
    5.90 -                | NONE => axiom_weight fudge loc const_tab rel_const_tab
    5.91 -                                       axiom_consts
    5.92 +                | NONE => fact_weight fudge loc const_tab rel_const_tab
    5.93 +                                      fact_consts
    5.94              in
    5.95                if weight >= threshold then
    5.96                  relevant ((ax, weight) :: candidates) rejects hopeful
    5.97 @@ -500,16 +500,16 @@
    5.98            relevant [] [] hopeful
    5.99          end
   5.100      fun add_add_ths accepts =
   5.101 -      (axioms |> filter ((member Thm.eq_thm add_ths
   5.102 -                          andf (not o member (Thm.eq_thm o apsnd snd) accepts))
   5.103 -                         o snd))
   5.104 +      (facts |> filter ((member Thm.eq_thm add_ths
   5.105 +                         andf (not o member (Thm.eq_thm o apsnd snd) accepts))
   5.106 +                        o snd))
   5.107        @ accepts
   5.108    in
   5.109 -    axioms |> map_filter (pair_consts_axiom thy irrelevant_consts fudge)
   5.110 -           |> iter 0 max_relevant threshold0 goal_const_tab []
   5.111 -           |> not (null add_ths) ? add_add_ths
   5.112 -           |> tap (fn res => trace_msg (fn () =>
   5.113 -                                "Total relevant: " ^ Int.toString (length res)))
   5.114 +    facts |> map_filter (pair_consts_fact thy irrelevant_consts fudge)
   5.115 +          |> iter 0 max_relevant threshold0 goal_const_tab []
   5.116 +          |> not (null add_ths) ? add_add_ths
   5.117 +          |> tap (fn res => trace_msg (fn () =>
   5.118 +                               "Total relevant: " ^ Int.toString (length res)))
   5.119    end
   5.120  
   5.121  
   5.122 @@ -793,7 +793,7 @@
   5.123                            1.0 / Real.fromInt (max_relevant + 1))
   5.124      val add_ths = Attrib.eval_thms ctxt add
   5.125      val reserved = reserved_isar_keyword_table ()
   5.126 -    val axioms =
   5.127 +    val facts =
   5.128        (if only then
   5.129           maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
   5.130                 o name_thm_pairs_from_ref ctxt reserved chained_ths) add
   5.131 @@ -802,16 +802,16 @@
   5.132        |> name_thm_pairs ctxt (respect_no_atp andalso not only)
   5.133        |> uniquify
   5.134    in
   5.135 -    trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
   5.136 -                        " theorems");
   5.137 +    trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^
   5.138 +                        " facts");
   5.139      (if only orelse threshold1 < 0.0 then
   5.140 -       axioms
   5.141 +       facts
   5.142       else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
   5.143               max_relevant = 0 then
   5.144         []
   5.145       else
   5.146         relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
   5.147 -                        fudge override axioms (concl_t :: hyp_ts))
   5.148 +                        fudge override facts (concl_t :: hyp_ts))
   5.149      |> map (apfst (apfst (fn f => f ())))
   5.150    end
   5.151  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 20:12:33 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 21:01:28 2010 +0200
     6.3 @@ -44,42 +44,42 @@
     6.4  
     6.5  fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
     6.6                   isar_shrink_factor, ...} : params) (prover : prover)
     6.7 -               explicit_apply timeout i n state axioms =
     6.8 +               explicit_apply timeout i n state facts =
     6.9    let
    6.10      val _ =
    6.11 -      Output.urgent_message ("Testing " ^ n_facts (map fst axioms) ^ "...")
    6.12 +      Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...")
    6.13      val params =
    6.14        {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
    6.15         provers = provers, full_types = full_types,
    6.16         explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
    6.17         max_relevant = NONE, isar_proof = isar_proof,
    6.18         isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
    6.19 -    val axioms =
    6.20 -      axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
    6.21 +    val facts =
    6.22 +      facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
    6.23      val {goal, ...} = Proof.goal state
    6.24      val problem =
    6.25        {state = state, goal = goal, subgoal = i, subgoal_count = n,
    6.26 -       axioms = axioms, only = true}
    6.27 -    val result as {outcome, used_axioms, ...} = prover params (K "") problem
    6.28 +       facts = facts, only = true}
    6.29 +    val result as {outcome, used_facts, ...} = prover params (K "") problem
    6.30    in
    6.31      Output.urgent_message (case outcome of
    6.32                  SOME failure => string_for_failure failure
    6.33                | NONE =>
    6.34 -                if length used_axioms = length axioms then "Found proof."
    6.35 -                else "Found proof with " ^ n_facts used_axioms ^ ".");
    6.36 +                if length used_facts = length facts then "Found proof."
    6.37 +                else "Found proof with " ^ n_facts used_facts ^ ".");
    6.38      result
    6.39    end
    6.40  
    6.41 -(* minimalization of thms *)
    6.42 +(* minimalization of facts *)
    6.43  
    6.44 -fun filter_used_axioms used = filter (member (op =) used o fst)
    6.45 +fun filter_used_facts used = filter (member (op =) used o fst)
    6.46  
    6.47  fun sublinear_minimize _ [] p = p
    6.48    | sublinear_minimize test (x :: xs) (seen, result) =
    6.49      case test (xs @ seen) of
    6.50 -      result as {outcome = NONE, used_axioms, ...} : prover_result =>
    6.51 -      sublinear_minimize test (filter_used_axioms used_axioms xs)
    6.52 -                         (filter_used_axioms used_axioms seen, result)
    6.53 +      result as {outcome = NONE, used_facts, ...} : prover_result =>
    6.54 +      sublinear_minimize test (filter_used_facts used_facts xs)
    6.55 +                         (filter_used_facts used_facts seen, result)
    6.56      | _ => sublinear_minimize test xs (x :: seen, result)
    6.57  
    6.58  (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
    6.59 @@ -89,7 +89,7 @@
    6.60  
    6.61  fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
    6.62    | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n
    6.63 -                   state axioms =
    6.64 +                   state facts =
    6.65    let
    6.66      val thy = Proof.theory_of state
    6.67      val prover = get_prover thy false prover_name
    6.68 @@ -99,13 +99,13 @@
    6.69      val (_, hyp_ts, concl_t) = strip_subgoal goal i
    6.70      val explicit_apply =
    6.71        not (forall (Meson.is_fol_term thy)
    6.72 -                  (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
    6.73 +                  (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
    6.74      fun do_test timeout =
    6.75        test_facts params prover explicit_apply timeout i n state
    6.76      val timer = Timer.startRealTimer ()
    6.77    in
    6.78 -    (case do_test timeout axioms of
    6.79 -       result as {outcome = NONE, used_axioms, ...} =>
    6.80 +    (case do_test timeout facts of
    6.81 +       result as {outcome = NONE, used_facts, ...} =>
    6.82         let
    6.83           val time = Timer.checkRealTimer timer
    6.84           val new_timeout =
    6.85 @@ -113,7 +113,7 @@
    6.86             |> Time.fromMilliseconds
    6.87           val (min_thms, {message, ...}) =
    6.88             sublinear_minimize (do_test new_timeout)
    6.89 -               (filter_used_axioms used_axioms axioms) ([], result)
    6.90 +               (filter_used_facts used_facts facts) ([], result)
    6.91           val n = length min_thms
    6.92           val _ = Output.urgent_message (cat_lines
    6.93             ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
    6.94 @@ -140,7 +140,7 @@
    6.95      val ctxt = Proof.context_of state
    6.96      val reserved = reserved_isar_keyword_table ()
    6.97      val chained_ths = #facts (Proof.goal state)
    6.98 -    val axioms =
    6.99 +    val facts =
   6.100        maps (map (apsnd single)
   6.101              o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
   6.102    in
   6.103 @@ -148,7 +148,7 @@
   6.104        0 => Output.urgent_message "No subgoal!"
   6.105      | n =>
   6.106        (kill_provers ();
   6.107 -       Output.urgent_message (#2 (minimize_facts params i n state axioms)))
   6.108 +       Output.urgent_message (#2 (minimize_facts params i n state facts)))
   6.109    end
   6.110  
   6.111  end;