src/HOL/Tools/Meson/meson.ML
changeset 42833 c0abc218b8b4
parent 42793 88bee9f6eec7
child 43264 a1a48c69d623
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue May 17 15:11:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 17 15:11:36 2011 +0200
     1.3 @@ -456,12 +456,13 @@
     1.4        [] => false (*not a function type, OK*)
     1.5      | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
     1.6  
     1.7 -(*Returns false if any Vars in the theorem mention type bool.
     1.8 -  Also rejects functions whose arguments are Booleans or other functions.*)
     1.9 +(* Returns false if any Vars in the theorem mention type bool.
    1.10 +   Also rejects functions whose arguments are Booleans or other functions. *)
    1.11  fun is_fol_term thy t =
    1.12 -    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
    1.13 +    Term.is_first_order [@{const_name all}, @{const_name All},
    1.14 +                         @{const_name Ex}] t andalso
    1.15      not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
    1.16 -                           | _ => false) t orelse
    1.17 +                          | _ => false) t orelse
    1.18           has_bool_arg_const t orelse
    1.19           exists_Const (higher_inst_const thy) t orelse
    1.20           has_meta_conn t);