has_consts renamed to has_conn, now actually parses the first-order formula
to avoid problems caused by connectives buried within descriptions and set comprehensions.

--- a/src/HOL/Tools/meson.ML	Sat Jul 15 18:17:47 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Sun Jul 16 14:26:22 2006 +0200
@@ -82,13 +82,15 @@
    | NONE => raise THM("forward_res", 0, [st]);
 
 
-(*Are any of the constants in "bs" present in the term?*)
-fun has_consts bs =
-  let fun has (Const(a,_)) = member (op =) bs a
-	| has (Const ("Hilbert_Choice.Eps",_) $ _) = false
-		     (*ignore constants within @-terms*)
-	| has (f$u) = has f orelse has u
-	| has (Abs(_,_,t)) = has t
+(*Are any of the logical connectives in "bs" present in the term?*)
+fun has_conns bs =
+  let fun has (Const(a,_)) = false
+        | has (Const("Trueprop",_) $ p) = has p
+        | has (Const("Not",_) $ p) = has p
+        | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
+        | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
+        | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
+        | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
 	| has _ = false
   in  has  end;
   
@@ -194,7 +196,7 @@
 fun cnf skoths (th,ths) =
   let fun cnf_aux (th,ths) =
   	if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
-        else if not (has_consts ["All","Ex","op &"] (prop_of th))  
+        else if not (has_conns ["All","Ex","op &"] (prop_of th))  
 	then th::ths (*no work to do, terminate*)
 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
 	    Const ("op &", _) => (*conjunction*)
@@ -410,7 +412,7 @@
 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   clauses that arise from a subgoal.*)
 fun skolemize th =
-  if not (has_consts ["Ex"] (prop_of th)) then th
+  if not (has_conns ["Ex"] (prop_of th)) then th
   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
                               disj_exD, disj_exD1, disj_exD2])))
     handle THM _ =>