1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Feb 04 07:40:02 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Feb 04 12:08:18 2012 +0100
     1.3 @@ -27,6 +27,7 @@
     1.4       type_enc: string option,
     1.5       strict: bool,
     1.6       lam_trans: string option,
     1.7 +     uncurried_aliases: bool option,
     1.8       relevance_thresholds: real * real,
     1.9       max_relevant: int option,
    1.10       max_mono_iters: int,
    1.11 @@ -147,7 +148,7 @@
    1.12    let val thy = Proof_Context.theory_of ctxt in
    1.13      case try (get_atp thy) name of
    1.14        SOME {best_slices, ...} =>
    1.15 -      exists (fn (_, (_, ((_, format, _, _), _))) => is_format format)
    1.16 +      exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format)
    1.17               (best_slices ctxt)
    1.18      | NONE => false
    1.19    end
    1.20 @@ -291,6 +292,7 @@
    1.21     type_enc: string option,
    1.22     strict: bool,
    1.23     lam_trans: string option,
    1.24 +   uncurried_aliases: bool option,
    1.25     relevance_thresholds: real * real,
    1.26     max_relevant: int option,
    1.27     max_mono_iters: int,
    1.28 @@ -581,9 +583,9 @@
    1.29          ({exec, required_execs, arguments, proof_delims, known_failures,
    1.30            conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
    1.31          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    1.32 -                    max_relevant, max_mono_iters, max_new_mono_instances,
    1.33 -                    isar_proof, isar_shrink_factor, slice, timeout,
    1.34 -                    preplay_timeout, ...})
    1.35 +                    uncurried_aliases, max_relevant, max_mono_iters,
    1.36 +                    max_new_mono_instances, isar_proof, isar_shrink_factor,
    1.37 +                    slice, timeout, preplay_timeout, ...})
    1.38          minimize_command
    1.39          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    1.40    let
    1.41 @@ -654,7 +656,8 @@
    1.42              fun run_slice time_left (cache_key, cache_value)
    1.43                      (slice, (time_frac, (complete,
    1.44                          (key as (best_max_relevant, format, best_type_enc,
    1.45 -                                 best_lam_trans), extra)))) =
    1.46 +                                 best_lam_trans, best_uncurried_aliases),
    1.47 +                                 extra)))) =
    1.48                let
    1.49                  val num_facts =
    1.50                    length facts |> is_none max_relevant
    1.51 @@ -687,6 +690,10 @@
    1.52                    case lam_trans of
    1.53                      SOME s => s
    1.54                    | NONE => best_lam_trans
    1.55 +                val uncurried_aliases =
    1.56 +                  case uncurried_aliases of
    1.57 +                    SOME b => b
    1.58 +                  | NONE => best_uncurried_aliases
    1.59                  val value as (atp_problem, _, fact_names, _, _) =
    1.60                    if cache_key = SOME key then
    1.61                      cache_value
    1.62 @@ -700,8 +707,8 @@
    1.63                         ? monomorphize_facts
    1.64                      |> map (apsnd prop_of)
    1.65                      |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
    1.66 -                           type_enc false lam_trans readable_names true hyp_ts
    1.67 -                           concl_t
    1.68 +                           type_enc false lam_trans uncurried_aliases
    1.69 +                           readable_names true hyp_ts concl_t
    1.70                  fun weights () = atp_problem_weights atp_problem
    1.71                  val full_proof = debug orelse isar_proof
    1.72                  val command =