1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 12 23:07:21 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 12:15:43 2013 +0100
     1.3 @@ -538,6 +538,9 @@
     1.4  fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 +    fun is_built_in (x as (s, _)) args =
     1.8 +      if member (op =) logical_consts s then (true, args)
     1.9 +      else is_built_in_const_for_prover ctxt prover x args
    1.10      val fixes = map snd (Variable.dest_fixes ctxt)
    1.11      val classes = Sign.classes_of thy
    1.12      fun add_classes @{sort type} = I
    1.13 @@ -554,45 +557,38 @@
    1.14        | do_add_type (TFree (_, S)) = add_classes S
    1.15        | do_add_type (TVar (_, S)) = add_classes S
    1.16      fun add_type T = type_max_depth >= 0 ? do_add_type T
    1.17 -    fun patternify_term _ 0 _ = ([], [])
    1.18 +    fun patternify_term _ 0 _ = []
    1.19        | patternify_term args _ (Const (x as (s, _))) =
    1.20 -        (if member (op =) logical_consts s then (true, args)
    1.21 -         else is_built_in_const_for_prover ctxt prover x args)
    1.22 -        |>> (fn true => [] | false => [s])
    1.23 -      | patternify_term args depth (Free (s, _)) =
    1.24 -        (if depth = term_max_depth andalso member (op =) fixes s then
    1.25 -           [thy_name ^ Long_Name.separator ^ s]
    1.26 -         else
    1.27 -           [], args)
    1.28 +        if fst (is_built_in x args) then [] else [s]
    1.29 +      | patternify_term _ depth (Free (s, _)) =
    1.30 +        if depth = term_max_depth andalso member (op =) fixes s then
    1.31 +          [thy_name ^ Long_Name.separator ^ s]
    1.32 +        else
    1.33 +          []
    1.34        | patternify_term args depth (t $ u) =
    1.35          let
    1.36 -          val (ps, u_args) =
    1.37 -            patternify_term (u :: args) depth t
    1.38 -            |>> take max_pattern_breadth
    1.39 -          val (qs, args) =
    1.40 -            case u_args of
    1.41 -              [] => ([], [])
    1.42 -            | arg :: args' =>
    1.43 -              if arg = u then
    1.44 -                (patternify_term [] (depth - 1) u
    1.45 -                 |> fst |> cons "" |> take max_pattern_breadth,
    1.46 -                 args')
    1.47 -              else
    1.48 -                ([], args')
    1.49 -        in
    1.50 -          (map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs,
    1.51 -           args)
    1.52 -        end
    1.53 -      | patternify_term _ _ _ = ([], [])
    1.54 +          val ps =
    1.55 +            take max_pattern_breadth (patternify_term (u :: args) depth t)
    1.56 +          val qs =
    1.57 +            take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u)
    1.58 +        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
    1.59 +      | patternify_term _ _ _ = []
    1.60      fun add_term_pattern feature_of =
    1.61 -      union (op = o pairself fst) o map feature_of o fst oo patternify_term []
    1.62 +      union (op = o pairself fst) o map feature_of oo patternify_term []
    1.63      fun add_term_patterns _ 0 _ = I
    1.64        | add_term_patterns feature_of depth t =
    1.65          add_term_pattern feature_of depth t
    1.66          #> add_term_patterns feature_of (depth - 1) t
    1.67      fun add_term feature_of = add_term_patterns feature_of term_max_depth
    1.68      fun add_patterns t =
    1.69 -      let val (head, args) = strip_comb t in
    1.70 +      case strip_comb t of
    1.71 +        (Const (x as (_, T)), args) =>
    1.72 +        let val (built_in, args) = is_built_in x args in
    1.73 +          (not built_in ? add_term const_feature_of t)
    1.74 +          #> add_type T
    1.75 +          #> fold add_patterns args
    1.76 +        end
    1.77 +      | (head, args) =>
    1.78          (case head of
    1.79             Const (_, T) => add_term const_feature_of t #> add_type T
    1.80           | Free (_, T) => add_term free_feature_of t #> add_type T
    1.81 @@ -600,7 +596,6 @@
    1.82           | Abs (_, T, body) => add_type T #> add_patterns body
    1.83           | _ => I)
    1.84          #> fold add_patterns args
    1.85 -      end
    1.86    in [] |> fold add_patterns ts end
    1.87  
    1.88  fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})