changeset 19305 | 5c16895d548b |
parent 19265 | cae36e16f3c0 |
child 19388 | 5cfa11eeddfe |
--- a/src/Pure/Thy/html.ML Tue Mar 21 12:18:13 2006 +0100 +++ b/src/Pure/Thy/html.ML Tue Mar 21 12:18:15 2006 +0100 @@ -223,7 +223,7 @@ in fun output_width str = - if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str) + if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) then Symbol.default_output str else let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))