--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:15:51 2011 +0100
@@ -11,7 +11,7 @@
val type_encK = "type_enc"
val soundK = "sound"
val slicingK = "slicing"
-val lambda_translationK = "lambda_translation"
+val lambda_transK = "lambda_trans"
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
@@ -355,9 +355,8 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method force_sos hard_timeout timeout dir
- pos st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+ 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
@@ -373,8 +372,8 @@
st |> Proof.map_context
(set_file_name dir
#> (Option.map (Config.put
- Sledgehammer_Provers.atp_lambda_translation)
- lambda_translation |> the_default I)
+ Sledgehammer_Provers.atp_lambda_trans)
+ lambda_trans |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
@@ -466,7 +465,7 @@
val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
- val lambda_translation = AList.lookup (op =) args lambda_translationK
+ val lambda_trans = AList.lookup (op =) args lambda_transK
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")
@@ -476,9 +475,8 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method force_sos hard_timeout timeout dir
- pos st
+ run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+ e_weight_method force_sos hard_timeout timeout dir pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:15:51 2011 +0100
@@ -243,7 +243,7 @@
fun generic_metis_tac type_syss ctxt ths i st0 =
let
- val lambda_trans = Config.get ctxt lambda_translation
+ val lambda_trans = Config.get ctxt lambda_trans
val _ = trace_msg ctxt (fn () =>
"Metis called with theorems\n" ^
cat_lines (map (Display.string_of_thm ctxt) ths))
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:15:51 2011 +0100
@@ -24,7 +24,7 @@
val metis_generated_var_prefix : string
val trace : bool Config.T
val verbose : bool Config.T
- val lambda_translation : string Config.T
+ val lambda_trans : string Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
@@ -52,9 +52,8 @@
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
-val lambda_translation =
- Attrib.setup_config_string @{binding metis_lambda_translation}
- (K combinatorsN)
+val lambda_trans =
+ Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:15:51 2011 +0100
@@ -62,7 +62,7 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
- val atp_lambda_translation : string Config.T
+ val atp_lambda_trans : string Config.T
val atp_full_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -339,9 +339,8 @@
val problem_prefix =
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val atp_lambda_translation =
- Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
- (K smartN)
+val atp_lambda_trans =
+ Attrib.setup_config_string @{binding sledgehammer_atp_lambda_trans} (K smartN)
(* In addition to being easier to read, readable names are often much shorter,
especially if types are mangled in names. This makes a difference for some
provers (e.g., E). For these reason, short names are enabled by default. *)
@@ -674,7 +673,7 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, _, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc false (Config.get ctxt atp_lambda_translation)
+ type_enc false (Config.get ctxt atp_lambda_trans)
(not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem