# HG changeset patch
# User wenzelm
# Date 1214940612 -7200
# Node ID 8a7100d33960449476604d93b6fff69c4a52f336
# Parent  b82c12e57e796bd6d85dae613f6ffdc9da9db0e7
tuned;

diff -r b82c12e57e79 -r 8a7100d33960 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Tue Jul 01 21:30:11 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Tue Jul 01 21:30:12 2008 +0200
@@ -75,7 +75,7 @@
 and get_pos (elem as XML.Elem (name, atts, ts)) =
       if name = Markup.positionN then SOME (Position.of_properties atts)
       else message_pos ts
-  | get_pos _ = NONE
+  | get_pos _ = NONE;
 
 in