# HG changeset patch
# User blanchet
# Date 1377153747 -7200
# Node ID a33298b49d9fbab6e73f5455b1f80aca984e35af
# Parent  98a2c33d5d1b36f87f6b3d773808065ed85d939c
tuning

diff -r 98a2c33d5d1b -r a33298b49d9f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 =
diff -r 98a2c33d5d1b -r a33298b49d9f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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