# HG changeset patch
# User wenzelm
# Date 1681503568 -7200
# Node ID ec50b9213969f6ecad3334496aea99aa0e5d0b31
# Parent  d589d1d218b25f6b11539252da589bd1eb558344
tuned;

diff -r d589d1d218b2 -r ec50b9213969 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/General/binding.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -209,7 +209,7 @@
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
-      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
+      exists (fn (a, _) => member (op =) bad_specs a orelse member_string a "\"") spec
       andalso error (bad binding);
 
     val spec' = if null spec2 then [] else spec;
diff -r d589d1d218b2 -r ec50b9213969 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -279,7 +279,7 @@
 val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
 
 fun thaw (T as TFree (a, S)) =
-      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
+      if member_string a ":" then TVar (unpack_ixn a, S) else T
   | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
   | thaw T = T;
 
diff -r d589d1d218b2 -r ec50b9213969 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/System/bash.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -43,7 +43,7 @@
           | "\r" => "$'\\r'"
           | _ =>
               if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
-                exists_string (fn c => c = ch) "+,-./:_" then ch
+                member_string "+,-./:_" ch then ch
               else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
               else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
               else "\\" ^ ch)
diff -r d589d1d218b2 -r ec50b9213969 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -85,7 +85,7 @@
       | "\n" => "\\isanewline\n"
       | s =>
           s
-          |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
+          |> member_string "\"#$%&',-<>\\^_`{}~" s ? enclose "{\\char`\\" "}"
           |> suffix "{\\kern0pt}");
 
 fun output_ascii_breakable sep =
@@ -203,7 +203,7 @@
   let
     val _ =
       citations |> List.app (fn (s, pos) =>
-        if exists_string (fn c => c = ",") s
+        if member_string s ","
         then error ("Single citation expected, without commas" ^ Position.here pos)
         else ());
     val citations' = space_implode "," (map #1 citations);
diff -r d589d1d218b2 -r ec50b9213969 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/library.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -771,7 +771,7 @@
 val trim_split_lines = trim_line #> split_lines #> map trim_line;
 
 fun normalize_lines str =
-  if exists_string (fn s => s = "\r") str then
+  if member_string str "\r" then
     split_lines str |> map trim_line |> cat_lines
   else str;