1.1 --- a/src/HOL/Tools/meson.ML	Wed Sep 13 12:05:50 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Sep 13 12:17:17 2006 +0200
     1.3 @@ -302,15 +302,14 @@
     1.4    | has_bool (Type(_, Ts)) = exists has_bool Ts
     1.5    | has_bool _ = false;
     1.6    
     1.7 -(*Is the string the name of a connective? It doesn't matter if this list is
     1.8 -  incomplete, since when actually called, the only connectives likely to
     1.9 -  remain are & | Not.*)  
    1.10 +(*Is the string the name of a connective? Really only | and Not can remain, 
    1.11 +  since this code expects to be called on a clause form.*)  
    1.12  val is_conn = member (op =)
    1.13 -    ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
    1.14 +    ["Trueprop", "op &", "op |", "op -->", "Not", 
    1.15       "All", "Ex", "Ball", "Bex"];
    1.16  
    1.17 -(*True if the term contains a function where the type of any argument contains
    1.18 -  bool.*)
    1.19 +(*True if the term contains a function--not a logical connective--where the type 
    1.20 +  of any argument contains bool.*)
    1.21  val has_bool_arg_const = 
    1.22      exists_Const
    1.23        (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));