# HG changeset patch
# User blanchet
# Date 1284455920 -7200
# Node ID fe84bc307be6a1d30c1f1f71d521cd8c5b751c45
# Parent  1ccc5c9ee343c9ab1f92a3e79fa37285b47ba9c2
speed up helper function

diff -r 1ccc5c9ee343 -r fe84bc307be6 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Sep 14 11:07:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Sep 14 11:18:40 2010 +0200
@@ -41,10 +41,10 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
-fun strip_spaces_in_list _ [] = ""
-  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
+fun strip_spaces_in_list _ [] = []
+  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
   | strip_spaces_in_list is_evil [c1, c2] =
-    strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
+    strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2]
   | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
     if Char.isSpace c1 then
       strip_spaces_in_list is_evil (c2 :: c3 :: cs)
@@ -52,11 +52,12 @@
       if Char.isSpace c3 then
         strip_spaces_in_list is_evil (c1 :: c3 :: cs)
       else
-        str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
+        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
         strip_spaces_in_list is_evil (c3 :: cs)
     else
-      str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
-fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
+      str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+fun strip_spaces is_evil =
+  implode o strip_spaces_in_list is_evil o String.explode
 
 val simplify_spaces = strip_spaces (K true)