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