src/HOL/ex/sledgehammer_tactics.ML
changeset 42638 a7a30721767a
parent 42589 9f7c48463645
child 42642 f5b4b9d4acda
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:31:46 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
     1.3 @@ -32,10 +32,8 @@
     1.4        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     1.5      val relevance_override = {add = [], del = [], only = false}
     1.6      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     1.7 -    val fairly_sound =
     1.8 -      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
     1.9      val facts =
    1.10 -      Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds
    1.11 +      Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.12            (the_default default_max_relevant max_relevant) is_built_in_const
    1.13            relevance_fudge relevance_override chained_ths hyp_ts concl_t
    1.14      val problem =