src/HOL/Tools/Meson/meson.ML

   val choice_theorems : theory -> thm list
   val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
   val skolemize : Proof.context -> thm -> thm
   val extensionalize_conv : Proof.context -> conv
   val extensionalize_theorem : Proof.context -> thm -> thm
-  val is_fol_term: theory -> term -> bool
   val make_clauses_unsorted: Proof.context -> thm list -> thm list
   val make_clauses: Proof.context -> thm list -> thm list
   val make_horns: thm list -> thm list
   val best_prolog_tac: (thm -> int) -> thm list -> tactic
   val depth_prolog_tac: thm list -> tactic

 fun higher_inst_const thy (c,T) =
   case binder_types T of
       [] => false (*not a function type, OK*)
     | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
 
-(* Returns false if any Vars in the theorem mention type bool.
-   Also rejects functions whose arguments are Booleans or other functions. *)
-fun is_fol_term thy t =
-    Term.is_first_order [@{const_name all}, @{const_name All},
-                         @{const_name Ex}] t andalso
-    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);
-
 fun rigid t = not (is_Var (head_of t));
 
 fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
   | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   | ok4horn _ = false;