# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID c0abc218b8b4b98df621f8039300278e55dc1b5b
# Parent  06afb3070af675da86796c2ec3d47db2ad29d773
use antiquotation

diff -r 06afb3070af6 -r c0abc218b8b4 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue May 17 15:11:36 2011 +0200
@@ -456,12 +456,13 @@
       [] => false (*not a function type, OK*)
     | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
 
-(*Returns false if any Vars in the theorem mention type bool.
-  Also rejects functions whose arguments are Booleans or other functions.*)
+(* Returns false if any Vars in the theorem mention type bool.
+   Also rejects functions whose arguments are Booleans or other functions. *)
 fun is_fol_term thy t =
-    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
+    Term.is_first_order [@{const_name all}, @{const_name All},
+                         @{const_name Ex}] t andalso
     not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
-                           | _ => false) t orelse
+                          | _ => false) t orelse
          has_bool_arg_const t orelse
          exists_Const (higher_inst_const thy) t orelse
          has_meta_conn t);