1.1 --- a/src/HOL/Tools/meson.ML Wed Feb 28 22:05:46 2007 +0100
1.2 +++ b/src/HOL/Tools/meson.ML Fri Mar 02 12:35:20 2007 +0100
1.3 @@ -354,13 +354,21 @@
1.4 val has_bool_arg_const =
1.5 exists_Const
1.6 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
1.7 -
1.8 +
1.9 +(*A higher-order instance of a first-order constant? Example is the definition of
1.10 + HOL.one, 1, at a function type in theory SetsAndFunctions.*)
1.11 +fun higher_inst_const thy (c,T) =
1.12 + case binder_types T of
1.13 + [] => false (*not a function type, OK*)
1.14 + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
1.15 +
1.16 (*Raises an exception if any Vars in the theorem mention type bool.
1.17 Also rejects functions whose arguments are Booleans or other functions.*)
1.18 -fun is_fol_term t =
1.19 +fun is_fol_term thy t =
1.20 + Term.is_first_order ["all","All","Ex"] t andalso
1.21 not (exists (has_bool o fastype_of) (term_vars t) orelse
1.22 - not (Term.is_first_order ["all","All","Ex"] t) orelse
1.23 has_bool_arg_const t orelse
1.24 + exists_Const (higher_inst_const thy) t orelse
1.25 has_meta_conn t);
1.26
1.27 fun rigid t = not (is_Var (head_of t));