# HG changeset patch
# User wenzelm
# Date 1218707705 -7200
# Node ID 827730aea9e863022a0019f21c733daa974f0c8b
# Parent  a084895d8b91f8590fad9e7f41c6304ec1341693
made SML/NJ happy;

diff -r a084895d8b91 -r 827730aea9e8 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Aug 13 20:57:40 2008 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Aug 14 11:55:05 2008 +0200
@@ -50,7 +50,7 @@
 val content = implode o map symbol;
 
 
-val tab_width = 8;
+val tab_width = (8: int);
 
 fun untabify ("\t", pos) =
       (case Position.column_of pos of