src/HOL/Tools/Meson/meson.ML
changeset 46818 2a28e66e2e4c
parent 46503 186f4cab2ba0
child 46904 f30e941b4512
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Mar 04 23:04:40 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Mar 04 23:20:43 2012 +0100
     1.3 @@ -26,7 +26,6 @@
     1.4    val skolemize : Proof.context -> thm -> thm
     1.5    val extensionalize_conv : Proof.context -> conv
     1.6    val extensionalize_theorem : Proof.context -> thm -> thm
     1.7 -  val is_fol_term: theory -> term -> bool
     1.8    val make_clauses_unsorted: Proof.context -> thm list -> thm list
     1.9    val make_clauses: Proof.context -> thm list -> thm list
    1.10    val make_horns: thm list -> thm list
    1.11 @@ -457,17 +456,6 @@
    1.12        [] => false (*not a function type, OK*)
    1.13      | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
    1.14  
    1.15 -(* Returns false if any Vars in the theorem mention type bool.
    1.16 -   Also rejects functions whose arguments are Booleans or other functions. *)
    1.17 -fun is_fol_term thy t =
    1.18 -    Term.is_first_order [@{const_name all}, @{const_name All},
    1.19 -                         @{const_name Ex}] t andalso
    1.20 -    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
    1.21 -                          | _ => false) t orelse
    1.22 -         has_bool_arg_const t orelse
    1.23 -         exists_Const (higher_inst_const thy) t orelse
    1.24 -         has_meta_conn t);
    1.25 -
    1.26  fun rigid t = not (is_Var (head_of t));
    1.27  
    1.28  fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t