diff -r 9fe826095a02 -r b86450f5b5cb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -254,11 +254,14 @@
 
 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
 
+val logical_consts =
+  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
+
 fun interesting_terms_types_and_classes ctxt prover term_max_depth
                                         type_max_depth ts =
   let
     fun is_bad_const (x as (s, _)) args =
-      member (op =) atp_logical_consts s orelse
+      member (op =) logical_consts s orelse
       fst (is_built_in_const_for_prover ctxt prover x args)
     fun add_classes @{sort type} = I
       | add_classes S = union (op =) (map class_name_of S)
@@ -274,8 +277,9 @@
     fun patternify ~1 _ = ""
       | patternify depth t =
         case strip_comb t of
-          (Const (s, _), args) =>
-          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
+          (Const (x as (s, _)), args) =>
+          if is_bad_const x args then ""
+          else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
         | _ => ""
     fun add_term_patterns ~1 _ = I
       | add_term_patterns depth t =
@@ -285,8 +289,7 @@
     fun add_patterns t =
       let val (head, args) = strip_comb t in
         (case head of
-           Const (x as (_, T)) =>
-           not (is_bad_const x args) ? (add_term t #> add_type T)
+           Const (_, T) => add_term t #> add_type T
          | Free (_, T) => add_type T
          | Var (_, T) => add_type T
          | Abs (_, T, body) => add_type T #> add_patterns body