treat frees as both consts and vars, for more hits
authorblanchet
Mon, 19 Aug 2013 23:22:04 +0200
changeset 53090 1426c97311f2
parent 53089 a58b3b8631c6
child 53091 d2afb0eb82e2
treat frees as both consts and vars, for more hits
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 21:59:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 23:22:04 2013 +0200
@@ -627,10 +627,11 @@
       | pattify_term _ args _ (Const (x as (s, _))) =
         if fst (is_built_in x args) then [] else [massage_long_name s]
       | pattify_term _ _ _ (Free (s, T)) =
-        if member (op =) fixes s then
-          [massage_long_name (thy_name ^ Long_Name.separator ^ s)]
-        else
-          [pat_var_prefix ^ crude_str_of_typ T]
+        [pat_var_prefix ^ crude_str_of_typ T]
+        |> (if member (op =) fixes s then
+              cons (massage_long_name (thy_name ^ Long_Name.separator ^ s))
+            else
+              I)
       | pattify_term _ _ _ (Var (_, T)) = [pat_var_prefix ^ crude_str_of_typ T]
       | pattify_term Ts _ _ (Bound j) =
         [pat_var_prefix ^ crude_str_of_typ (nth Ts j)]