src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55208 11dd3d1da83b
parent 55207 42ad887a1c7c
child 55211 5d027af93a08
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:32:13 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:42:47 2014 +0100
     1.3 @@ -77,9 +77,6 @@
     1.4    val is_reconstructor : string -> bool
     1.5    val is_atp : theory -> string -> bool
     1.6    val is_ho_atp: Proof.context -> string -> bool
     1.7 -  val is_unit_equational_atp : Proof.context -> string -> bool
     1.8 -  val is_unit_equality : term -> bool
     1.9 -  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
    1.10    val supported_provers : Proof.context -> unit
    1.11    val kill_provers : unit -> unit
    1.12    val running_provers : unit -> unit
    1.13 @@ -146,7 +143,6 @@
    1.14      | NONE => false)
    1.15    end
    1.16  
    1.17 -val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
    1.18  val is_ho_atp = is_atp_of_format is_format_higher_order
    1.19  
    1.20  fun remotify_atp_if_supported_and_not_already_remote thy name =
    1.21 @@ -161,28 +157,6 @@
    1.22    if is_atp thy name andalso is_atp_installed thy name then SOME name
    1.23    else remotify_atp_if_supported_and_not_already_remote thy name
    1.24  
    1.25 -fun is_if (@{const_name If}, _) = true
    1.26 -  | is_if _ = false
    1.27 -
    1.28 -(* Beware of "if and only if" (which is translated as such) and "If" (which is
    1.29 -   translated to conditional equations). *)
    1.30 -fun is_good_unit_equality T t u =
    1.31 -  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
    1.32 -
    1.33 -fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
    1.34 -  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
    1.35 -    is_unit_equality t
    1.36 -  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    1.37 -    is_unit_equality t
    1.38 -  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
    1.39 -    is_good_unit_equality T t u
    1.40 -  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
    1.41 -    is_good_unit_equality T t u
    1.42 -  | is_unit_equality _ = false
    1.43 -
    1.44 -fun is_appropriate_prop_of_prover ctxt name =
    1.45 -  if is_unit_equational_atp ctxt name then is_unit_equality else K true
    1.46 -
    1.47  fun supported_provers ctxt =
    1.48    let
    1.49      val thy = Proof_Context.theory_of ctxt