--- a/src/HOL/Tools/meson.ML Thu Jul 29 21:20:24 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 29 22:13:15 2010 +0200
@@ -390,10 +390,13 @@
fun sort_clauses ths = sort (make_ord fewerlits) ths;
-(*True if the given type contains bool anywhere*)
-fun has_bool (Type("bool",_)) = true
- | has_bool (Type(_, Ts)) = exists has_bool Ts
- | has_bool _ = false;
+fun has_bool @{typ bool} = true
+ | has_bool (Type (_, Ts)) = exists has_bool Ts
+ | has_bool _ = false
+
+fun has_fun (Type (@{type_name fun}, _)) = true
+ | has_fun (Type (_, Ts)) = exists has_fun Ts
+ | has_fun _ = false
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
@@ -405,7 +408,7 @@
of any argument contains bool.*)
val has_bool_arg_const =
exists_Const
- (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
+ (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
(*A higher-order instance of a first-order constant? Example is the definition of
one, 1, at a function type in theory SetsAndFunctions.*)
@@ -418,8 +421,9 @@
Also rejects functions whose arguments are Booleans or other functions.*)
fun is_fol_term thy t =
Term.is_first_order ["all","All","Ex"] t andalso
- not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse
- has_bool_arg_const t orelse
+ not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
+ | _ => false) t orelse
+ has_bool_arg_const t orelse
exists_Const (higher_inst_const thy) t orelse
has_meta_conn t);