src/Pure/Thy/html.ML

--- 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))