# HG changeset patch
# User wenzelm
# Date 904482882 -7200
# Node ID 0a0a35dddabdb407e146f7ef2d474dbfd6d19f52
# Parent  b450fea6d70cd268a81495852d46226f560096d8
made SML/NJ happy;

diff -r b450fea6d70c -r 0a0a35dddabd src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Fri Aug 28 15:01:13 1998 +0200
+++ b/src/Pure/Syntax/token_trans.ML	Sun Aug 30 15:14:42 1998 +0200
@@ -134,7 +134,7 @@
 (* FIXME 'a -> \alpha etc. *)
 
 val latex_trans =
- trans_mode "latex" [];
+ trans_mode "latex" [] : (string * string * (string -> string * int)) list;