src/Pure/Thy/html.ML
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);