1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -254,11 +254,14 @@
     1.4  
     1.5  val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
     1.6  
     1.7 +val logical_consts =
     1.8 +  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
     1.9 +
    1.10  fun interesting_terms_types_and_classes ctxt prover term_max_depth
    1.11                                          type_max_depth ts =
    1.12    let
    1.13      fun is_bad_const (x as (s, _)) args =
    1.14 -      member (op =) atp_logical_consts s orelse
    1.15 +      member (op =) logical_consts s orelse
    1.16        fst (is_built_in_const_for_prover ctxt prover x args)
    1.17      fun add_classes @{sort type} = I
    1.18        | add_classes S = union (op =) (map class_name_of S)
    1.19 @@ -274,8 +277,9 @@
    1.20      fun patternify ~1 _ = ""
    1.21        | patternify depth t =
    1.22          case strip_comb t of
    1.23 -          (Const (s, _), args) =>
    1.24 -          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
    1.25 +          (Const (x as (s, _)), args) =>
    1.26 +          if is_bad_const x args then ""
    1.27 +          else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
    1.28          | _ => ""
    1.29      fun add_term_patterns ~1 _ = I
    1.30        | add_term_patterns depth t =
    1.31 @@ -285,8 +289,7 @@
    1.32      fun add_patterns t =
    1.33        let val (head, args) = strip_comb t in
    1.34          (case head of
    1.35 -           Const (x as (_, T)) =>
    1.36 -           not (is_bad_const x args) ? (add_term t #> add_type T)
    1.37 +           Const (_, T) => add_term t #> add_type T
    1.38           | Free (_, T) => add_type T
    1.39           | Var (_, T) => add_type T
    1.40           | Abs (_, T, body) => add_type T #> add_patterns body