src/Pure/General/binding.ML
changeset 77851 ec50b9213969
parent 77841 de97fcc2c624
child 77949 0290a9879b03
--- 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;