use antiquotation
authorblanchet
Tue May 17 15:11:36 2011 +0200 (2011-05-17)
changeset 42833c0abc218b8b4
parent 42832 06afb3070af6
child 42834 40f7691d0539
use antiquotation
src/HOL/Tools/Meson/meson.ML
     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);