1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:52 2014 +0200
     1.3 @@ -1206,8 +1206,7 @@
     1.4            let
     1.5              val chunks = app_hd (cons th) chunks
     1.6              val chunks_and_parents' =
     1.7 -              if thm_less_eq (th, th') andalso
     1.8 -                 thy_name_of_thm th = thy_name_of_thm th' then
     1.9 +              if thm_less_eq (th, th') andalso thy_name_of_thm th = thy_name_of_thm th' then
    1.10                  (chunks, [nickname_of_thm th])
    1.11                else
    1.12                  chunks_and_parents_for chunks th'
    1.13 @@ -1254,7 +1253,7 @@
    1.14  
    1.15  val chained_feature_factor = 0.5 (* FUDGE *)
    1.16  val extra_feature_factor = 0.1 (* FUDGE *)
    1.17 -val num_extra_feature_facts = 10 (* FUDGE *)
    1.18 +val num_extra_feature_facts = 0 (* FUDGE *) (* TODO: keep or eliminate? *)
    1.19  
    1.20  (* FUDGE *)
    1.21  fun weight_of_proximity_fact rank =