# HG changeset patch
# User blanchet
# Date 1368020839 -7200
# Node ID 097b191d1f0de1f2a005a06da87aff05fe7834de
# Parent  3c152334f79464792b1be7ef994cfc7a860ee056
use right default for "uncurried_aliases" with polymorphic SPASS

diff -r 3c152334f794 -r 097b191d1f0d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 08 13:33:04 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 08 15:47:19 2013 +0200
@@ -610,7 +610,7 @@
 
 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
 
-fun dummy_config prem_role format type_enc : atp_config =
+fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
    arguments = K (K (K (K (K (K ""))))),
    proof_delims = [],
@@ -619,19 +619,19 @@
    best_slices =
      K [(1.0, (((200, ""), format, type_enc,
                 if is_format_higher_order format then keep_lamsN
-                else combsN, false), ""))],
+                else combsN, uncurried_aliases), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_thf_format =
   THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
 val dummy_thf_config =
-  dummy_config Hypothesis dummy_thf_format "poly_native_higher"
+  dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
 
 val spass_poly_format = DFG Polymorphic
 val spass_poly_config =
-  dummy_config (#prem_role spass_config) spass_poly_format "tc_native"
+  dummy_config (#prem_role spass_config) spass_poly_format "tc_native" true
 val spass_poly = (spass_polyN, fn () => spass_poly_config)
 
 (* Remote ATP invocation via SystemOnTPTP *)