diff -r fd03765b06c0 -r e1abca2527da src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:29:48 2014 +0200
@@ -9,7 +9,7 @@
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   val reports_of_tokens: Token.T list -> bool * Position.report_text list
   val present_token: Token.T -> Output.output
-  datatype span_kind = Command of string * Position.T | Ignored | Malformed
+  datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
   datatype span = Span of span_kind * Token.T list
   val span_kind: span -> span_kind
   val span_content: span -> Token.T list
@@ -69,9 +69,7 @@
 
 (** spans **)
 
-(* type span *)
-
-datatype span_kind = Command of string * Position.T | Ignored | Malformed;
+datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
 datatype span = Span of span_kind * Token.T list;
 
 fun span_kind (Span (k, _)) = k;
@@ -84,27 +82,29 @@
 
 local
 
-fun make_span toks =
-  if not (null toks) andalso Token.is_command (hd toks) then
-    Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
-  else if forall Token.is_improper toks then Span (Ignored, toks)
-  else Span (Malformed, toks);
+fun ship span =
+  let
+    val kind =
+      if not (null span) andalso Token.is_command (hd span) then
+        Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
+      else if forall Token.is_improper span then Ignored_Span
+      else Malformed_Span;
+  in cons (Span (kind, span)) end;
 
-fun flush (result, span, improper) =
+fun flush (result, content, improper) =
   result
-  |> not (null span) ? cons (rev span)
-  |> not (null improper) ? cons (rev improper);
+  |> not (null content) ? ship (rev content)
+  |> not (null improper) ? ship (rev improper);
 
-fun parse tok (result, span, improper) =
-  if Token.is_command tok then (flush (result, span, improper), [tok], [])
-  else if Token.is_improper tok then (result, span, tok :: improper)
-  else (result, tok :: (improper @ span), []);
+fun parse tok (result, content, improper) =
+  if Token.is_command tok then (flush (result, content, improper), [tok], [])
+  else if Token.is_improper tok then (result, content, tok :: improper)
+  else (result, tok :: (improper @ content), []);
 
 in
 
 fun parse_spans toks =
-  fold parse toks ([], [], [])
-  |> flush |> rev |> map make_span;
+  fold parse toks ([], [], []) |> flush |> rev;
 
 end;
 
@@ -137,7 +137,7 @@
 
 fun resolve_files read_files span =
   (case span of
-    Span (Command (cmd, pos), toks) =>
+    Span (Command_Span (cmd, pos), toks) =>
       if Keyword.is_theory_load cmd then
         (case find_file (clean_tokens toks) of
           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
@@ -146,7 +146,7 @@
               val toks' = toks |> map_index (fn (j, tok) =>
                 if i = j then Token.put_files (read_files cmd path) tok
                 else tok);
-            in Span (Command (cmd, pos), toks') end)
+            in Span (Command_Span (cmd, pos), toks') end)
       else span
   | _ => span);
 
@@ -174,9 +174,9 @@
 
 (* scanning spans *)
 
-val eof = Span (Command ("", Position.none), []);
+val eof = Span (Command_Span ("", Position.none), []);
 
-fun is_eof (Span (Command ("", _), _)) = true
+fun is_eof (Span (Command_Span ("", _), _)) = true
   | is_eof _ = false;
 
 val not_eof = not o is_eof;
@@ -189,10 +189,10 @@
 local
 
 fun command_with pred =
-  Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
+  Scan.one (fn (Span (Command_Span (name, _), _)) => pred name | _ => false);
 
 val proof_atom =
-  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
+  Scan.one (fn (Span (Command_Span (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
 
 fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
 and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;