# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID a6ed27399ba97139ea46fe831d4f8407964e9378
# Parent  f99ee3adb81d40f36eb2205c50010b1ae75a52ff
avoid double traversal of term

diff -r f99ee3adb81d -r a6ed27399ba9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -203,15 +203,13 @@
    "Random_Sequence", "Sledgehammer", "SMT"]
   |> map (suffix Long_Name.separator)
 
-fun has_technical_prefix s =
+fun is_technical_const (s, _) =
   exists (fn pref => String.isPrefix pref s) technical_prefixes
-val exists_technical_const = exists_Const (has_technical_prefix o fst)
 
 (* FIXME: make more reliable *)
-val exists_low_level_class_const =
-  exists_Const (fn (s, _) =>
-     s = @{const_name equal_class.equal} orelse
-     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
+val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
+fun is_low_level_class_const (s, _) =
+  s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
 
 fun is_that_fact th =
   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
@@ -241,8 +239,9 @@
   in
     (is_boring_prop [] (prop_of th) andalso
      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
-    exists_type type_has_top_sort t orelse exists_technical_const t orelse
-    exists_low_level_class_const t orelse is_that_fact th
+    exists_type type_has_top_sort t orelse
+    exists_Const (is_technical_const orf is_low_level_class_const) t orelse
+    is_that_fact th
   end
 
 fun is_blacklisted_or_something ctxt ho_atp name =