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;