changeset 26435 | bdce320cd426 |
parent 26323 | 73efc70edeef |
child 26463 | 9283b4185fdf |
--- a/src/Pure/Thy/html.ML Thu Mar 27 15:32:12 2008 +0100 +++ b/src/Pure/Thy/html.ML Thu Mar 27 15:32:15 2008 +0100 @@ -267,7 +267,7 @@ ("var", var_or_skolem), ("xstr", style "xstr")]; -val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans); +val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);