src/HOL/ex/sledgehammer_tactics.ML
changeset 42589 9f7c48463645
parent 42579 2552c09b1a72
child 42638 a7a30721767a
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -32,9 +32,10 @@
     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 half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
     1.8 +    val fairly_sound =
     1.9 +      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
    1.10      val facts =
    1.11 -      Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds
    1.12 +      Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds
    1.13            (the_default default_max_relevant max_relevant) is_built_in_const
    1.14            relevance_fudge relevance_override chained_ths hyp_ts concl_t
    1.15      val problem =