1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -131,8 +131,7 @@
     1.4    val type_constrs_of_terms : theory -> term list -> string list
     1.5    val prepare_atp_problem :
     1.6      Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     1.7 -    -> bool option -> bool -> bool -> term list -> term
     1.8 -    -> ((string * locality) * term) list
     1.9 +    -> bool -> bool -> term list -> term -> ((string * locality) * term) list
    1.10      -> string problem * string Symtab.table * int * int
    1.11         * (string * locality) list vector * int list * int Symtab.table
    1.12    val atp_problem_weights : string problem -> (string * real) list
    1.13 @@ -1833,9 +1832,10 @@
    1.14  val conjsN = "Conjectures"
    1.15  val free_typesN = "Type variables"
    1.16  
    1.17 +val explicit_apply = NONE (* for experimental purposes *)
    1.18 +
    1.19  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
    1.20 -                        explicit_apply readable_names preproc hyp_ts concl_t
    1.21 -                        facts =
    1.22 +                        readable_names preproc hyp_ts concl_t facts =
    1.23    let
    1.24      val (format, type_sys) = choose_format [format] type_sys
    1.25      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =

     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
     2.3 @@ -706,7 +706,7 @@
     2.4        val ax_counts =
     2.5          Int_Tysubst_Table.empty
     2.6          |> fold (fn (ax_no, (_, (tysubst, _))) =>
     2.7 -                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
     2.8 +                    Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0)
     2.9                                                    (Integer.add 1)) substs
    2.10          |> Int_Tysubst_Table.dest
    2.11        val needed_axiom_props =

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     3.3 @@ -167,7 +167,6 @@
     3.4  fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
     3.5    let
     3.6      val type_sys = type_sys_from_string type_sys
     3.7 -    val explicit_apply = NONE
     3.8      val clauses =
     3.9        conj_clauses @ fact_clauses
    3.10        |> (if polymorphism_of_type_sys type_sys = Polymorphic then
    3.11 @@ -188,8 +187,8 @@
    3.12  val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
    3.13  *)
    3.14      val (atp_problem, _, _, _, _, _, sym_tab) =
    3.15 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
    3.16 -                          false false props @{prop False} []
    3.17 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
    3.18 +                          @{prop False} []
    3.19  (*
    3.20  val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
    3.21  *)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
     4.3 @@ -96,7 +96,6 @@
     4.4     ("max_relevant", "smart"),
     4.5     ("max_mono_iters", "3"),
     4.6     ("max_new_mono_instances", "400"),
     4.7 -   ("explicit_apply", "smart"),
     4.8     ("isar_proof", "false"),
     4.9     ("isar_shrink_factor", "1"),
    4.10     ("slicing", "true"),
    4.11 @@ -112,14 +111,13 @@
    4.12     ("no_overlord", "overlord"),
    4.13     ("non_blocking", "blocking"),
    4.14     ("partial_types", "full_types"),
    4.15 -   ("implicit_apply", "explicit_apply"),
    4.16     ("no_isar_proof", "isar_proof"),
    4.17     ("no_slicing", "slicing")]
    4.18  
    4.19  val params_for_minimize =
    4.20    ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    4.21 -   "max_new_mono_instances", "explicit_apply", "isar_proof",
    4.22 -   "isar_shrink_factor", "timeout", "preplay_timeout"]
    4.23 +   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    4.24 +   "preplay_timeout"]
    4.25  
    4.26  val property_dependent_params = ["provers", "full_types", "timeout"]
    4.27  
    4.28 @@ -284,7 +282,6 @@
    4.29      val max_relevant = lookup_option lookup_int "max_relevant"
    4.30      val max_mono_iters = lookup_int "max_mono_iters"
    4.31      val max_new_mono_instances = lookup_int "max_new_mono_instances"
    4.32 -    val explicit_apply = lookup_option lookup_bool "explicit_apply"
    4.33      val isar_proof = lookup_bool "isar_proof"
    4.34      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    4.35      val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
    4.36 @@ -299,9 +296,9 @@
    4.37       provers = provers, relevance_thresholds = relevance_thresholds,
    4.38       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    4.39       max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    4.40 -     explicit_apply = explicit_apply, isar_proof = isar_proof,
    4.41 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    4.42 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    4.43 +     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    4.44 +     slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
    4.45 +     expect = expect}
    4.46    end
    4.47  
    4.48  fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
     5.3 @@ -47,7 +47,7 @@
     5.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     5.5  
     5.6  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     5.7 -                 max_new_mono_instances, type_sys, explicit_apply, isar_proof,
     5.8 +                 max_new_mono_instances, type_sys, isar_proof,
     5.9                   isar_shrink_factor, preplay_timeout, ...} : params)
    5.10                 silent (prover : prover) timeout i n state facts =
    5.11    let
    5.12 @@ -59,7 +59,7 @@
    5.13      val {goal, ...} = Proof.goal state
    5.14      val params =
    5.15        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    5.16 -       provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    5.17 +       provers = provers, type_sys = type_sys,
    5.18         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    5.19         max_mono_iters = max_mono_iters,
    5.20         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    5.21 @@ -73,16 +73,18 @@
    5.22      val result as {outcome, used_facts, run_time_in_msecs, ...} =
    5.23        prover params (K (K "")) problem
    5.24    in
    5.25 -    print silent (fn () =>
    5.26 -        case outcome of
    5.27 -          SOME failure => string_for_failure failure
    5.28 -        | NONE => "Found proof" ^
    5.29 -                  (if length used_facts = length facts then ""
    5.30 -                   else " with " ^ n_facts used_facts) ^
    5.31 -                  (case run_time_in_msecs of
    5.32 -                     SOME ms =>
    5.33 -                     " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
    5.34 -                   | NONE => "") ^ ".");
    5.35 +    print silent
    5.36 +          (fn () =>
    5.37 +              case outcome of
    5.38 +                SOME failure => string_for_failure failure
    5.39 +              | NONE =>
    5.40 +                "Found proof" ^
    5.41 +                 (if length used_facts = length facts then ""
    5.42 +                  else " with " ^ n_facts used_facts) ^
    5.43 +                 (case run_time_in_msecs of
    5.44 +                    SOME ms =>
    5.45 +                    " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
    5.46 +                  | NONE => "") ^ ".");
    5.47      result
    5.48    end
    5.49  

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
     6.3 @@ -33,7 +33,6 @@
     6.4       max_relevant: int option,
     6.5       max_mono_iters: int,
     6.6       max_new_mono_instances: int,
     6.7 -     explicit_apply: bool option,
     6.8       isar_proof: bool,
     6.9       isar_shrink_factor: int,
    6.10       slicing: bool,
    6.11 @@ -301,7 +300,6 @@
    6.12     max_relevant: int option,
    6.13     max_mono_iters: int,
    6.14     max_new_mono_instances: int,
    6.15 -   explicit_apply: bool option,
    6.16     isar_proof: bool,
    6.17     isar_shrink_factor: int,
    6.18     slicing: bool,
    6.19 @@ -549,8 +547,8 @@
    6.20          ({exec, required_execs, arguments, proof_delims, known_failures,
    6.21            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    6.22          ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
    6.23 -          max_new_mono_instances, explicit_apply, isar_proof,
    6.24 -          isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
    6.25 +          max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
    6.26 +          timeout, preplay_timeout, ...} : params)
    6.27          minimize_command
    6.28          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    6.29    let
    6.30 @@ -655,9 +653,8 @@
    6.31                  val (atp_problem, pool, conjecture_offset, facts_offset,
    6.32                       fact_names, typed_helpers, sym_tab) =
    6.33                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    6.34 -                      type_sys explicit_apply
    6.35 -                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
    6.36 -                      facts
    6.37 +                      type_sys (Config.get ctxt atp_readable_names) true hyp_ts
    6.38 +                      concl_t facts
    6.39                  fun weights () = atp_problem_weights atp_problem
    6.40                  val core =
    6.41                    File.shell_path command ^ " " ^

     7.1 --- a/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
     7.2 +++ b/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
     7.3 @@ -102,11 +102,10 @@
     7.4      val facts =
     7.5        facts0 |> map (fn ((_, loc), th) =>
     7.6                          ((Thm.get_name_hint th, loc), prop_of th))
     7.7 -    val explicit_apply = NONE
     7.8      val (atp_problem, _, _, _, _, _, _) =
     7.9        ATP_Translate.prepare_atp_problem ctxt format
    7.10 -          ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
    7.11 -          [] @{prop False} facts
    7.12 +          ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true []
    7.13 +          @{prop False} facts
    7.14      val infers =
    7.15        facts0 |> map (fn (_, th) =>
    7.16                          (fact_name_of (Thm.get_name_hint th),