--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 08:42:27 2013 +0200
@@ -509,7 +509,6 @@
end
fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
-fun const_feature_of s = ("c" ^ s, 32.0 (* FUDGE *))
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
@@ -680,7 +679,7 @@
fun add_term Ts = add_term_pats Ts term_max_depth
fun add_subterms Ts t =
case strip_comb t of
- (Const (x as (s, T)), args) =>
+ (Const (x as (_, T)), args) =>
let val (built_in, args) = is_built_in x args in
(not built_in ? add_term Ts t)
#> add_subtypes T
@@ -818,10 +817,6 @@
(*** High-level communication with MaSh ***)
-fun attach_crude_parents_to_facts _ [] = []
- | attach_crude_parents_to_facts parents ((fact as (_, th)) :: facts) =
- (parents, fact) :: attach_crude_parents_to_facts [nickname_of_thm th] facts
-
(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
fun chunks_and_parents_for chunks th =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Aug 22 08:42:27 2013 +0200
@@ -687,9 +687,9 @@
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_compress,
- isar_compress_degree, merge_timeout_slack,
- isar_try0, isar_minimize,
- slice, timeout, preplay_timeout, preplay_trace, ...})
+ isar_compress_degree, merge_timeout_slack, isar_try0,
+ isar_minimize, slice, timeout, preplay_timeout,
+ preplay_trace, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -966,8 +966,8 @@
val isar_params =
(debug, verbose, preplay_timeout, preplay_trace,
isar_compress, isar_compress_degree, merge_timeout_slack,
- isar_try0,isar_minimize,
- pool, fact_names, lifted, sym_tab, atp_proof, goal)
+ isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab,
+ atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command ctxt params minimize_command name