1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -155,51 +155,6 @@
     1.4  val type_name_of = prefix type_const_prefix
     1.5  val class_name_of = prefix class_prefix
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun has_bool @{typ bool} = true
    1.10 -  | has_bool (Type (_, Ts)) = exists has_bool Ts
    1.11 -  | has_bool _ = false
    1.12 -
    1.13 -fun has_fun (Type (@{type_name fun}, _)) = true
    1.14 -  | has_fun (Type (_, Ts)) = exists has_fun Ts
    1.15 -  | has_fun _ = false
    1.16 -
    1.17 -val is_conn = member (op =)
    1.18 -  [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
    1.19 -   @{const_name HOL.implies}, @{const_name Not},
    1.20 -   @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
    1.21 -   @{const_name HOL.eq}]
    1.22 -
    1.23 -val has_bool_arg_const =
    1.24 -  exists_Const (fn (c, T) =>
    1.25 -                   not (is_conn c) andalso exists has_bool (binder_types T))
    1.26 -
    1.27 -fun higher_inst_const thy (s, T) =
    1.28 -  case binder_types T of
    1.29 -    [] => false
    1.30 -  | Ts => length (binder_types (Sign.the_const_type thy s)) <> length Ts
    1.31 -  handle TYPE _ => false
    1.32 -
    1.33 -val binders = [@{const_name All}, @{const_name Ex}]
    1.34 -
    1.35 -in
    1.36 -
    1.37 -fun is_fo_term thy t =
    1.38 -  let
    1.39 -    val t =
    1.40 -      t |> Envir.beta_eta_contract
    1.41 -        |> transform_elim_prop
    1.42 -        |> Object_Logic.atomize_term thy
    1.43 -  in
    1.44 -    Term.is_first_order binders t andalso
    1.45 -    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
    1.46 -                          | _ => false) t orelse
    1.47 -         has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
    1.48 -  end
    1.49 -
    1.50 -end
    1.51 -
    1.52  fun is_likely_tautology_or_too_meta th =
    1.53    let
    1.54      val is_boring_const = member (op =) atp_widely_irrelevant_consts
    1.55 @@ -285,7 +240,6 @@
    1.56                                        ts
    1.57    |> exists (not o is_lambda_free) ts ? cons "lambdas"
    1.58    |> exists (exists_Const is_exists) ts ? cons "skolems"
    1.59 -  |> exists (not o is_fo_term thy) ts ? cons "ho"
    1.60    |> (case status of
    1.61          General => I
    1.62        | Induction => cons "induction"