Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/latex.ML
changeset 77851 ec50b9213969
parent 77768 65008644d394 
--- 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);
isabelle