# HG changeset patch
# User paulson
# Date 1158142637 -7200
# Node ID 1493053fc111eeda92376ed92f063708ed469074
# Parent  36a59e5d003909cbe7fa6ab921689a433b3c8fad
Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
since this test is applied to clause forms.

diff -r 36a59e5d0039 -r 1493053fc111 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Sep 13 12:05:50 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Sep 13 12:17:17 2006 +0200
@@ -302,15 +302,14 @@
   | has_bool (Type(_, Ts)) = exists has_bool Ts
   | has_bool _ = false;
   
-(*Is the string the name of a connective? It doesn't matter if this list is
-  incomplete, since when actually called, the only connectives likely to
-  remain are & | Not.*)  
+(*Is the string the name of a connective? Really only | and Not can remain, 
+  since this code expects to be called on a clause form.*)  
 val is_conn = member (op =)
-    ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
+    ["Trueprop", "op &", "op |", "op -->", "Not", 
      "All", "Ex", "Ball", "Bex"];
 
-(*True if the term contains a function where the type of any argument contains
-  bool.*)
+(*True if the term contains a function--not a logical connective--where the type 
+  of any argument contains bool.*)
 val has_bool_arg_const = 
     exists_Const
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));