made option available to users (mostly for experiments)

--- a/NEWS	Sat Feb 04 07:40:02 2012 +0100
+++ b/NEWS	Sat Feb 04 12:08:18 2012 +0100
@@ -305,7 +305,7 @@
     affecting 'rat' and 'real'.
 
 * Sledgehammer:
-  - Added "lam_trans" and "minimize" options.
+  - Added "lam_trans", "uncurry_aliases", and "minimize" options.
   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
   - Renamed "sound" option to "strict".
 

--- a/doc-src/Sledgehammer/sledgehammer.tex	Sat Feb 04 07:40:02 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Sat Feb 04 12:08:18 2012 +0100
@@ -722,6 +722,7 @@
 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -1005,6 +1006,10 @@
 For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
 irrespective of the value of this option.
 
+\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
+Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
+translation schemes are listed below:
+
 \opdefault{type\_enc}{string}{smart}
 Specifies the type encoding to use in ATP problems. Some of the type encodings
 are unsound, meaning that they can give rise to spurious proofs

--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -181,7 +181,7 @@
                  ((Thm.get_name_hint th, loc),
                    th |> prop_of |> mono ? monomorphize_term ctxt))
       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
-                             true [] @{prop False}
+                             false true [] @{prop False}
       |> #1
     val atp_problem =
       atp_problem

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -103,7 +103,7 @@
   val factsN : string
   val prepare_atp_problem :
     Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-    -> bool -> string -> bool -> bool -> term list -> term
+    -> bool -> string -> bool -> bool -> bool -> term list -> term
     -> ((string * stature) * term) list
     -> string problem * string Symtab.table * (string * stature) list vector
        * (string * term) list * int Symtab.table
@@ -166,7 +166,7 @@
 val sym_decl_prefix = "sy_"
 val guards_sym_formula_prefix = "gsy_"
 val tags_sym_formula_prefix = "tsy_"
-val app_op_alias_eq_prefix = "aa_"
+val uncurried_alias_eq_prefix = "unc_"
 val fact_prefix = "fact_"
 val conjecture_prefix = "conj_"
 val helper_prefix = "help_"
@@ -875,10 +875,10 @@
   if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
 
 (* This shouldn't clash with anything else. *)
-val app_op_alias_sep = "\000"
+val uncurried_alias_sep = "\000"
 val mangled_type_sep = "\001"
 
-val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep
+val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
 
 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   | generic_mangled_type_name f (ATerm (name, tys)) =
@@ -919,10 +919,10 @@
   ho_type_from_ho_term type_enc pred_sym ary
   o ho_term_from_typ format type_enc
 
-fun aliased_app_op ary (s, s') =
-  (s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
-fun unaliased_app_op (s, s') =
-  case space_explode app_op_alias_sep s of
+fun aliased_uncurried ary (s, s') =
+  (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
+fun unaliased_uncurried (s, s') =
+  case space_explode uncurried_alias_sep s of
     [_] => (s, s')
   | [s1, s2] => (s1, unsuffix s2 s')
   | _ => raise Fail "ill-formed explicit application alias"
@@ -955,7 +955,7 @@
     |> fst
 
 fun unmangled_const_name s =
-  (s, s) |> unaliased_app_op |> fst |> space_explode mangled_type_sep
+  (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
 fun unmangled_const s =
   let val ss = unmangled_const_name s in
     (hd ss, map unmangled_type (tl ss))
@@ -1533,7 +1533,7 @@
   in list_app app [head, arg] end
 
 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
-                       app_op_aliases =
+                       uncurried_aliases =
   let
     fun do_app arg head = do_app_op format type_enc head arg
     fun list_app_ops head args = fold do_app args head
@@ -1541,10 +1541,11 @@
       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
         case head of
           IConst (name as (s, _), T, T_args) =>
-          if app_op_aliases andalso String.isPrefix const_prefix s then
+          if uncurried_aliases andalso String.isPrefix const_prefix s then
             let
               val ary = length args
-              val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary
+              val name = name |> ary > min_ary_of sym_tab s
+                                 ? aliased_uncurried ary
             in list_app (IConst (name, T, T_args)) args end
           else
             args |> chop (min_ary_of sym_tab s)
@@ -2393,8 +2394,8 @@
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
-fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
-        type_enc sym_tab0 sym_tab base_s0 types in_conj =
+fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
+        mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
   let
     fun do_alias ary =
       let
@@ -2412,8 +2413,8 @@
         fun do_const name = IConst (name, T, T_args)
         val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true)
         val name1 as (s1, _) =
-          base_name |> ary - 1 > base_ary ? aliased_app_op (ary - 1)
-        val name2 as (s2, _) = base_name |> aliased_app_op ary
+          base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
+        val name2 as (s2, _) = base_name |> aliased_uncurried ary
         val (arg_Ts, _) = chop_fun ary T
         val bound_names =
           1 upto ary |> map (`I o make_bound_var o string_of_int)
@@ -2431,35 +2432,35 @@
                      (do_term tm1) (do_term tm2)
       in
         ([tm1, tm2],
-         [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE,
-                   isabelle_info format spec_eqN helper_rank)])
+         [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
+                   NONE, isabelle_info format spec_eqN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
   in do_alias end
-fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
-                               type_enc sym_tab0 sym_tab
-                               (s, {min_ary, types, in_conj, ...} : sym_info) =
+fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
+        type_enc sym_tab0 sym_tab
+        (s, {min_ary, types, in_conj, ...} : sym_info) =
   case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
-    if String.isSubstring app_op_alias_sep mangled_s then
+    if String.isSubstring uncurried_alias_sep mangled_s then
       let
         val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
       in
-        do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
+        do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
             mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
       end
     else
       ([], [])
   | NONE => ([], [])
-fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
-        mono type_enc app_op_aliases sym_tab0 sym_tab =
+fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
+        mono type_enc uncurried_aliases sym_tab0 sym_tab =
   ([], [])
-  |> app_op_aliases
+  |> uncurried_aliases
      ? Symtab.fold_rev
            (pair_append
-            o app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
-                  mono type_enc sym_tab0 sym_tab) sym_tab
+            o uncurried_alias_lines_for_sym ctxt monom_constrs format
+                  conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
 
 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
     Config.get ctxt type_tag_idempotence andalso
@@ -2469,7 +2470,7 @@
 
 val implicit_declsN = "Should-be-implicit typings"
 val explicit_declsN = "Explicit typings"
-val app_op_alias_eqsN = "Application aliases"
+val uncurried_alias_eqsN = "Uncurried aliases"
 val factsN = "Relevant facts"
 val class_relsN = "Class relationships"
 val aritiesN = "Arities"
@@ -2554,7 +2555,8 @@
 val app_op_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
-                        lam_trans readable_names preproc hyp_ts concl_t facts =
+                        lam_trans uncurried_aliases readable_names preproc
+                        hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
@@ -2568,7 +2570,6 @@
         Incomplete_Apply
       else
         Sufficient_Apply
-    val app_op_aliases = (format = DFG DFG_Sorted)
     val lam_trans =
       if lam_trans = keep_lamsN andalso
          not (is_type_enc_higher_order type_enc) then
@@ -2587,7 +2588,7 @@
       |>> map (make_fixed_const (SOME format))
     fun firstorderize in_helper =
       firstorderize_fact thy monom_constrs format type_enc sym_tab0
-                         (app_op_aliases andalso not in_helper)
+                         (uncurried_aliases andalso not in_helper)
     val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
     val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
     val helpers =
@@ -2596,11 +2597,11 @@
     val mono_Ts =
       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
     val class_decl_lines = decl_lines_for_classes type_enc classes
-    val (app_op_alias_eq_tms, app_op_alias_eq_lines) =
-      app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
-          mono type_enc app_op_aliases sym_tab0 sym_tab
+    val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
+      uncurried_alias_lines_for_sym_table ctxt monom_constrs format
+          conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
     val sym_decl_lines =
-      (conjs, helpers @ facts, app_op_alias_eq_tms)
+      (conjs, helpers @ facts, uncurried_alias_eq_tms)
       |> sym_decl_table_for_facts ctxt format type_enc sym_tab
       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
                                                type_enc mono_Ts
@@ -2622,7 +2623,7 @@
        FLOTTER hack. *)
     val problem =
       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
-       (app_op_alias_eqsN, app_op_alias_eq_lines),
+       (uncurried_alias_eqsN, uncurried_alias_eq_lines),
        (factsN, fact_lines),
        (class_relsN,
         map (formula_line_for_class_rel_clause format type_enc)

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -11,6 +11,7 @@
   type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
+  type slice_spec = int * atp_format * string * string * bool
   type atp_config =
     {exec : string * string,
      required_execs : (string * string) list,
@@ -22,9 +23,7 @@
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
-       Proof.context
-       -> (real * (bool * ((int * atp_format * string * string) * string)))
-            list}
+       Proof.context -> (real * (bool * (slice_spec * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
@@ -58,8 +57,7 @@
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (failure * string) list -> formula_kind -> formula_kind
-    -> (Proof.context -> int * atp_format * string * string)
-    -> string * atp_config
+    -> (Proof.context -> slice_spec) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -77,6 +75,8 @@
 
 (* ATP configuration *)
 
+type slice_spec = int * atp_format * string * string * bool
+
 type atp_config =
   {exec : string * string,
    required_execs : (string * string) list,
@@ -87,17 +87,16 @@
    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
-   best_slices :
-     Proof.context
-     -> (real * (bool * ((int * atp_format * string * string) * string))) list}
+   best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" component gives the faction of the
-   time available given to the slice and should add up to 1.0. The "bool"
+   time available given to the slice and should add up to 1.0. The first "bool"
    component indicates whether the slice's strategy is complete; the "int", the
    preferred number of facts to pass; the first "string", the preferred type
    system (which should be sound or quasi-sound); the second "string", the
-   preferred lambda translation scheme; the third "string", extra information to
+   preferred lambda translation scheme; the second "bool", whether uncurried
+   aliased should be generated; the third "string", extra information to
    the prover (e.g., SOS or no SOS).
 
    The last slice should be the most "normal" one, because it will get all the
@@ -248,12 +247,14 @@
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
-          (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
-          (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
+         [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
+                          e_fun_weightN))),
+          (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
+                          e_fun_weightN))),
+          (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
                           e_sym_offset_weightN)))]
        else
-         [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
+         [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
      end}
 
 val e = (eN, e_config)
@@ -278,9 +279,9 @@
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
+     [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
                        sosN))),
-      (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
+      (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
                       no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
@@ -305,8 +306,8 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
-                      "")))]}
+     K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
+                       false), "")))]}
 
 val satallax = (satallaxN, satallax_config)
 
@@ -338,20 +339,20 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
+     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
                        sosN))),
-      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
+      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
                        sosN))),
-      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
+      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
                        no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val spass = (spassN, spass_config)
 
-val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
-val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
-val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
+val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
 
 (* Experimental *)
 val spass_new_config : atp_config =
@@ -368,9 +369,9 @@
    prem_kind = #prem_kind spass_config,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.300, (true, (spass_new_macro_slice_1, ""))),
-      (0.333, (true, (spass_new_macro_slice_2, ""))),
-      (0.333, (true, (spass_new_macro_slice_3, "")))]}
+     [(0.300, (true, (spass_new_slice_1, ""))),
+      (0.333, (true, (spass_new_slice_2, ""))),
+      (0.333, (true, (spass_new_slice_3, "")))]}
 
 val spass_new = (spass_newN, spass_new_config)
 
@@ -410,18 +411,19 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_old_vampire_version () then
-        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
-                           sosN))),
-         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
-         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
+        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
+                          sosN))),
+         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
+                          sosN))),
+         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
                          no_sosN)))]
       else
         [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
-                           combs_or_liftingN), sosN))),
-         (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
-                          sosN))),
-         (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
-                         no_sosN)))])
+                           combs_or_liftingN, false), sosN))),
+         (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
+                           false), sosN))),
+         (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
+                          false), no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -443,10 +445,10 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
-        (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
-        (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
-        (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
+     K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
@@ -464,7 +466,7 @@
    best_slices =
      K [(1.0, (false, ((200, format, type_enc,
                         if is_format_higher_order format then keep_lamsN
-                        else combsN), "")))]}
+                        else combsN, false), "")))]}
 
 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
@@ -515,16 +517,13 @@
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
-     ^ " -s " ^ the_system system_name system_versions,
+     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+     " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
-   best_slices = fn ctxt =>
-     let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
-       [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
-     end}
+   best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
 
 fun remotify_config system_name system_versions best_slice
         ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
@@ -545,43 +544,44 @@
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-      (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
+      (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-      (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
+      (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-      (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
+      (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
+         (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
-      (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
+      (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
 val remote_z3_tptp =
   remotify_atp z3_tptp "Z3" ["3.0"]
-      (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
+      (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-      Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
+      Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
 val remote_iprover =
   remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
-      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+      (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
 val remote_iprover_eq =
   remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
-      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+      (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
       [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-      (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+      (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
       Hypothesis
-      (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+      (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
       [("#START OF PROOF", "Proved Goals:")]
       [(OutOfResources, "Too many function symbols"),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
-      (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
+      (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
 
 (* Setup *)
 

--- a/src/HOL/Tools/Metis/metis_generate.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -242,7 +242,7 @@
     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
     val (atp_problem, _, _, lifted, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
-                          false false [] @{prop False} props
+                          false false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (lines_for_atp_problem CNF atp_problem))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -89,6 +89,7 @@
    ("type_enc", "smart"),
    ("strict", "false"),
    ("lam_trans", "smart"),
+   ("uncurried_aliases", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
    ("max_mono_iters", "3"),
@@ -107,14 +108,15 @@
    ("no_overlord", "overlord"),
    ("non_blocking", "blocking"),
    ("non_strict", "strict"),
+   ("no_uncurried_aliases", "uncurried_aliases"),
    ("no_isar_proof", "isar_proof"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
-   "max_mono_iters", "max_new_mono_instances", "isar_proof",
-   "isar_shrink_factor", "timeout", "preplay_timeout"]
+   "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
+   "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -286,6 +288,7 @@
       | s => (type_enc_from_string Strict s; SOME s)
     val strict = mode = Auto_Try orelse lookup_bool "strict"
     val lam_trans = lookup_option lookup_string "lam_trans"
+    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_option lookup_int "max_relevant"
     val max_mono_iters = lookup_int "max_mono_iters"
@@ -304,8 +307,9 @@
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, type_enc = type_enc, strict = strict,
-     lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
-     max_relevant = max_relevant, max_mono_iters = max_mono_iters,
+     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
+     max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -48,7 +48,8 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
-                 isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
+                 uncurried_aliases, isar_proof, isar_shrink_factor,
+                 preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
     val _ =
@@ -62,8 +63,9 @@
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_enc = type_enc, strict = strict,
-       lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
-       max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
+       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+       relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
+       max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slice = false,
        minimize = SOME false, timeout = timeout,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -27,6 +27,7 @@
      type_enc: string option,
      strict: bool,
      lam_trans: string option,
+     uncurried_aliases: bool option,
      relevance_thresholds: real * real,
      max_relevant: int option,
      max_mono_iters: int,
@@ -147,7 +148,7 @@
   let val thy = Proof_Context.theory_of ctxt in
     case try (get_atp thy) name of
       SOME {best_slices, ...} =>
-      exists (fn (_, (_, ((_, format, _, _), _))) => is_format format)
+      exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format)
              (best_slices ctxt)
     | NONE => false
   end
@@ -291,6 +292,7 @@
    type_enc: string option,
    strict: bool,
    lam_trans: string option,
+   uncurried_aliases: bool option,
    relevance_thresholds: real * real,
    max_relevant: int option,
    max_mono_iters: int,
@@ -581,9 +583,9 @@
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
-                    max_relevant, max_mono_iters, max_new_mono_instances,
-                    isar_proof, isar_shrink_factor, slice, timeout,
-                    preplay_timeout, ...})
+                    uncurried_aliases, max_relevant, max_mono_iters,
+                    max_new_mono_instances, isar_proof, isar_shrink_factor,
+                    slice, timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
@@ -654,7 +656,8 @@
             fun run_slice time_left (cache_key, cache_value)
                     (slice, (time_frac, (complete,
                         (key as (best_max_relevant, format, best_type_enc,
-                                 best_lam_trans), extra)))) =
+                                 best_lam_trans, best_uncurried_aliases),
+                                 extra)))) =
               let
                 val num_facts =
                   length facts |> is_none max_relevant
@@ -687,6 +690,10 @@
                   case lam_trans of
                     SOME s => s
                   | NONE => best_lam_trans
+                val uncurried_aliases =
+                  case uncurried_aliases of
+                    SOME b => b
+                  | NONE => best_uncurried_aliases
                 val value as (atp_problem, _, fact_names, _, _) =
                   if cache_key = SOME key then
                     cache_value
@@ -700,8 +707,8 @@
                        ? monomorphize_facts
                     |> map (apsnd prop_of)
                     |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                           type_enc false lam_trans readable_names true hyp_ts
-                           concl_t
+                           type_enc false lam_trans uncurried_aliases
+                           readable_names true hyp_ts concl_t
                 fun weights () = atp_problem_weights atp_problem
                 val full_proof = debug orelse isar_proof
                 val command =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Feb 04 07:40:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -74,9 +74,9 @@
 
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
-         lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
-         max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
-         minimize, timeout, preplay_timeout, expect} : params) =
+         lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
+         max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
+         slice, minimize, timeout, preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -89,8 +89,8 @@
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, type_enc = type_enc, strict = strict,
-     lam_trans = lam_trans, max_relevant = max_relevant,
-     relevance_thresholds = relevance_thresholds,
+     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+     max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
      max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slice = slice,