1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Feb 04 07:40:02 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Feb 04 12:08:18 2012 +0100
     1.3 @@ -89,6 +89,7 @@
     1.4     ("type_enc", "smart"),
     1.5     ("strict", "false"),
     1.6     ("lam_trans", "smart"),
     1.7 +   ("uncurried_aliases", "smart"),
     1.8     ("relevance_thresholds", "0.45 0.85"),
     1.9     ("max_relevant", "smart"),
    1.10     ("max_mono_iters", "3"),
    1.11 @@ -107,14 +108,15 @@
    1.12     ("no_overlord", "overlord"),
    1.13     ("non_blocking", "blocking"),
    1.14     ("non_strict", "strict"),
    1.15 +   ("no_uncurried_aliases", "uncurried_aliases"),
    1.16     ("no_isar_proof", "isar_proof"),
    1.17     ("dont_slice", "slice"),
    1.18     ("dont_minimize", "minimize")]
    1.19  
    1.20  val params_for_minimize =
    1.21    ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    1.22 -   "max_mono_iters", "max_new_mono_instances", "isar_proof",
    1.23 -   "isar_shrink_factor", "timeout", "preplay_timeout"]
    1.24 +   "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
    1.25 +   "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"]
    1.26  
    1.27  val property_dependent_params = ["provers", "timeout"]
    1.28  
    1.29 @@ -286,6 +288,7 @@
    1.30        | s => (type_enc_from_string Strict s; SOME s)
    1.31      val strict = mode = Auto_Try orelse lookup_bool "strict"
    1.32      val lam_trans = lookup_option lookup_string "lam_trans"
    1.33 +    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    1.34      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.35      val max_relevant = lookup_option lookup_int "max_relevant"
    1.36      val max_mono_iters = lookup_int "max_mono_iters"
    1.37 @@ -304,8 +307,9 @@
    1.38    in
    1.39      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.40       provers = provers, type_enc = type_enc, strict = strict,
    1.41 -     lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
    1.42 -     max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    1.43 +     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    1.44 +     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    1.45 +     max_mono_iters = max_mono_iters,
    1.46       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    1.47       isar_shrink_factor = isar_shrink_factor, slice = slice,
    1.48       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,