# HG changeset patch
# User blanchet
# Date 1376947324 -7200
# Node ID 1426c97311f26cf6d03270e56f6526342d1f579d
# Parent  a58b3b8631c6caf288653b649123b62ea7e9c27f
treat frees as both consts and vars, for more hits

diff -r a58b3b8631c6 -r 1426c97311f2 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)]