made SML/NJ happy;
authorwenzelm
Sun Aug 30 15:14:42 1998 +0200 (1998-08-30)
changeset 54080a0a35dddabd
parent 5407 b450fea6d70c
child 5409 e97558ee8e76
made SML/NJ happy;
src/Pure/Syntax/token_trans.ML
     1.1 --- a/src/Pure/Syntax/token_trans.ML	Fri Aug 28 15:01:13 1998 +0200
     1.2 +++ b/src/Pure/Syntax/token_trans.ML	Sun Aug 30 15:14:42 1998 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  (* FIXME 'a -> \alpha etc. *)
     1.5  
     1.6  val latex_trans =
     1.7 - trans_mode "latex" [];
     1.8 + trans_mode "latex" [] : (string * string * (string -> string * int)) list;
     1.9  
    1.10  
    1.11