src/Pure/Thy/html.ML
changeset 17221 6cd180204582
parent 17209 2ae243868a62
child 17412 e26cb20ef0cc
--- a/src/Pure/Thy/html.ML	Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Thy/html.ML	Thu Sep 01 18:48:50 2005 +0200
@@ -205,7 +205,7 @@
   fun output_sym s =
     if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
     else
-      (case Symtab.lookup (html_syms, s) of SOME x => x
+      (case Symtab.curried_lookup html_syms s of SOME x => x
       | NONE => (real (size s), translate_string escape s));
 
   fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);