src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

           |> sh_minimizeLST (*don't confuse the two minimization flags*)
           |> max_new_mono_instancesLST
           |> max_mono_itersLST)
     val default_max_facts =
       Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
-    val is_appropriate_prop =
-      Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))

         message = K "", message_tail = ""}, ~1)
     val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
          : Sledgehammer_Prover.prover_result,
          time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
-        val _ = if is_appropriate_prop concl_t then ()
-                else raise Fail "inappropriate"
         val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name
         val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
         val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
         val facts =
           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
               Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
               hyp_ts concl_t
         val factss =
           facts
-          |> filter (is_appropriate_prop o prop_of o snd)
           |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
           |> tap (fn factss =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^