# HG changeset patch
# User blanchet
# Date 1328371285 -3600
# Node ID 26153cbe97bf5053265a8ed5eb1720b6dafcf208
# Parent  4ed12518fb8148090b4124a011b0f80f8336d74d
added option to Mirabelle/Sledgehammer

diff -r 4ed12518fb81 -r 26153cbe97bf src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Feb 04 12:08:18 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Feb 04 17:01:25 2012 +0100
@@ -12,6 +12,7 @@
 val strictK = "strict"
 val sliceK = "slice"
 val lam_transK = "lam_trans"
+val uncurried_aliasesK = "uncurried_aliases"
 val e_weight_methodK = "e_weight_method"
 val force_sosK = "force_sos"
 val max_relevantK = "max_relevant"
@@ -362,7 +363,8 @@
   SH_ERROR
 
 fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
-        e_weight_method force_sos hard_timeout timeout dir pos st =
+        uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
+        st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -387,6 +389,7 @@
            ("type_enc", type_enc),
            ("strict", strict),
            ("lam_trans", lam_trans |> the_default "smart"),
+           ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
            ("preplay_timeout", preplay_timeout),
            ("max_relevant", max_relevant),
            ("slice", slice),
@@ -471,6 +474,7 @@
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slice = AList.lookup (op =) args sliceK |> the_default "true"
     val lam_trans = AList.lookup (op =) args lam_transK
+    val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
     val e_weight_method = AList.lookup (op =) args e_weight_methodK
     val force_sos = AList.lookup (op =) args force_sosK
       |> Option.map (curry (op <>) "false")
@@ -481,7 +485,8 @@
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_enc strict max_relevant slice lam_trans
-        e_weight_method force_sos hard_timeout timeout dir pos st
+        uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
+        st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>