tuned;

--- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 20 14:09:09 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 20 14:23:20 2012 +0200
@@ -13,8 +13,8 @@
   type span
   val span_kind: span -> span_kind
   val span_content: span -> Token.T list
+  val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
-  val present_span: span -> Output.output
   type element = {head: span, proof: span list, proper_proof: bool}
   val parse_elements: span list -> element list
 end;
@@ -106,6 +106,8 @@
 fun span_kind (Span (k, _)) = k;
 fun span_content (Span (_, toks)) = toks;
 
+val present_span = implode o map present_token o span_content;
+
 
 (* parse *)
 
@@ -129,11 +131,6 @@
 end;
 
 
-(* present *)
-
-val present_span = implode o map present_token o span_content;
-
-
 
 (** specification elements: commands with optional proof **)