# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID cf7679195169c9a67bfd605d086bce72b289cc8a
# Parent  8d8f72aa5c0b9bc114374a127c3be8fcc376b5d8
minor speed optimization

diff -r 8d8f72aa5c0b -r cf7679195169 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
@@ -211,8 +211,10 @@
 fun is_low_level_class_const (s, _) =
   s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
 
+val sep_that = Long_Name.separator ^ Obtain.thatN
+
 fun is_that_fact th =
-  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
+  String.isSuffix sep_that (Thm.get_name_hint th)
   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
                            | _ => false) (prop_of th)