# HG changeset patch
# User blanchet
# Date 1386558210 -3600
# Node ID dd5874e4553fa894790151408f7828cf63c774ae
# Parent  5ce1b96137058bff883a61748cc92ecba3bbe816
more reasonable default weight

diff -r 5ce1b9613705 -r dd5874e4553f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 09 04:03:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 09 04:03:30 2013 +0100
@@ -519,6 +519,7 @@
             |> map snd |> take max_facts
     end
 
+val default_weight = 1.0
 fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
 fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
 fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
@@ -642,20 +643,20 @@
         if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
       | pattify_term _ _ (Free (s, T)) =
         maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
-        |> map (rpair 0.0)
+        |> map (rpair 1.0)
         |> (if member (op =) fixes s then
               cons (free_feature_of (massage_long_name
                   (thy_name ^ Long_Name.separator ^ s)))
             else
               I)
       | pattify_term _ _ (Var (_, T)) =
-        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair 0.0)
+        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
       | pattify_term Ts _ (Bound j) =
-        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair 0.0)
+        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair default_weight)
       | pattify_term Ts depth (t $ u) =
         let
           val ps = take max_pat_breadth (pattify_term Ts depth t)
-          val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth - 1) u)
+          val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
         in
           map_product (fn ppw as (p, pw) =>
               fn ("", _) => ppw