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));