# HG changeset patch
# User wenzelm
# Date 1124270123 -7200
# Node ID f708a31fa8bb62fc2506fdb2d9d0369ea8e924e8
# Parent  3f797ec16f02ef2936a512b466bb42eb41fb8a32
made SML/XL happy;

diff -r 3f797ec16f02 -r f708a31fa8bb src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed Aug 17 08:06:12 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Wed Aug 17 11:15:23 2005 +0200
@@ -206,13 +206,14 @@
 (* command spans *)
 
 type command = string * Position.T * string list;   (*name, position, tags*)
-type source = (string * token * int) list;          (*raw text, token, meta-comment depth*)
+type tok = string * token * int;                    (*raw text, token, meta-comment depth*)
+type source = tok list;          
 
 datatype span = Span of command * (source * source * source * source) * bool;
 
 fun make_span cmd src =
   let
-    fun take_newline (tok :: toks) =
+    fun take_newline ((tok: tok) :: toks) =
           if newline_token (#2 tok) then ([tok], toks, true)
           else ([], tok :: toks, false)
       | take_newline [] = ([], [], false);