avoid double traversal of term
authorblanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53507a6ed27399ba9
parent 53506 f99ee3adb81d
child 53508 8d8f72aa5c0b
avoid double traversal of term
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -203,15 +203,13 @@
     1.4     "Random_Sequence", "Sledgehammer", "SMT"]
     1.5    |> map (suffix Long_Name.separator)
     1.6  
     1.7 -fun has_technical_prefix s =
     1.8 +fun is_technical_const (s, _) =
     1.9    exists (fn pref => String.isPrefix pref s) technical_prefixes
    1.10 -val exists_technical_const = exists_Const (has_technical_prefix o fst)
    1.11  
    1.12  (* FIXME: make more reliable *)
    1.13 -val exists_low_level_class_const =
    1.14 -  exists_Const (fn (s, _) =>
    1.15 -     s = @{const_name equal_class.equal} orelse
    1.16 -     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
    1.17 +val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
    1.18 +fun is_low_level_class_const (s, _) =
    1.19 +  s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
    1.20  
    1.21  fun is_that_fact th =
    1.22    String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
    1.23 @@ -241,8 +239,9 @@
    1.24    in
    1.25      (is_boring_prop [] (prop_of th) andalso
    1.26       not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
    1.27 -    exists_type type_has_top_sort t orelse exists_technical_const t orelse
    1.28 -    exists_low_level_class_const t orelse is_that_fact th
    1.29 +    exists_type type_has_top_sort t orelse
    1.30 +    exists_Const (is_technical_const orf is_low_level_class_const) t orelse
    1.31 +    is_that_fact th
    1.32    end
    1.33  
    1.34  fun is_blacklisted_or_something ctxt ho_atp name =