src/Pure/Thy/html.ML

     | output_syms (s :: ss) = output_sym s :: output_syms ss
     | output_syms [] = [];
 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))
       (output_syms (Symbol.explode str)) 0.0
     in (implode syms, width) end;