1.1 --- a/src/Pure/Thy/html.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4  in
     1.5  
     1.6  fun output_width str =
     1.7 -  if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str)
     1.8 +  if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
     1.9    then Symbol.default_output str
    1.10    else
    1.11      let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))