src/Pure/Thy/thy_syntax.ML

--- a/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -18,6 +18,7 @@
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
+  val last_element: 'a element -> 'a
   val parse_elements: span list -> span element list
 end;
 
@@ -148,6 +149,9 @@
 fun flat_element (Element (a, NONE)) = [a]
   | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
 
+fun last_element (Element (a, NONE)) = a
+  | last_element (Element (_, SOME (_, b))) = b;
+
 
 (* scanning spans *)