src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 38652 e063be321438
parent 38644 25bbbaf7ce65
child 38679 2cfd0777580f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:51:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:54:17 2010 +0200
     1.3 @@ -23,6 +23,8 @@
     1.4  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
     1.5  struct
     1.6  
     1.7 +open Sledgehammer_Util
     1.8 +
     1.9  val trace = Unsynchronized.ref false
    1.10  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    1.11  
    1.12 @@ -43,7 +45,7 @@
    1.13      val name = Facts.string_of_ref xref
    1.14                 |> forall (member Thm.eq_thm chained_ths) ths
    1.15                    ? prefix chained_prefix
    1.16 -  in (name, ths |> map Clausifier.transform_elim_theorem) end
    1.17 +  in (name, ths) end
    1.18  
    1.19  
    1.20  (***************************************************************)
    1.21 @@ -420,7 +422,7 @@
    1.22  val exists_sledgehammer_const =
    1.23    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    1.24  
    1.25 -fun is_strange_thm th =
    1.26 +fun is_strange_theorem th =
    1.27    case head_of (concl_of th) of
    1.28        Const (a, _) => (a <> @{const_name Trueprop} andalso
    1.29                         a <> @{const_name "=="})
    1.30 @@ -486,13 +488,15 @@
    1.31     are omitted. *)
    1.32  fun is_dangerous_term full_types t =
    1.33    not full_types andalso
    1.34 -  (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
    1.35 +  ((has_bound_or_var_of_type dangerous_types t andalso
    1.36 +    has_bound_or_var_of_type dangerous_types (transform_elim_term t))
    1.37 +   orelse is_exhaustive_finite t)
    1.38  
    1.39  fun is_theorem_bad_for_atps full_types thm =
    1.40    let val t = prop_of thm in
    1.41      is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    1.42      is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
    1.43 -    is_strange_thm thm
    1.44 +    is_strange_theorem thm
    1.45    end
    1.46  
    1.47  fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
    1.48 @@ -525,8 +529,7 @@
    1.49              val name1 = Facts.extern facts name;
    1.50              val name2 = Name_Space.extern full_space name;
    1.51              val ths =
    1.52 -              ths0 |> map Clausifier.transform_elim_theorem
    1.53 -                   |> filter ((not o is_theorem_bad_for_atps full_types) orf
    1.54 +              ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
    1.55                                member Thm.eq_thm add_thms)
    1.56              val name' =
    1.57                case find_first check_thms [name1, name2, name] of
    1.58 @@ -538,7 +541,7 @@
    1.59                                           (prop_of th) ^ "`")
    1.60                      |> space_implode " "
    1.61            in
    1.62 -            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
    1.63 +            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
    1.64                             ? prefix chained_prefix, ths)
    1.65            end)
    1.66    in