print assertions in a more natural order

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Dec 11 22:31:24 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Dec 13 23:37:37 2009 +0100
@@ -59,6 +59,8 @@
 
 fun write_list head pp xs = Pretty.writeln (Pretty.big_list head (map pp xs))
 
+val prefix_string_ord = dict_ord string_ord o pairself explode
+
 fun boogie_status thy =
   let
     fun string_of_state Boogie_VCs.Proved = "proved"
@@ -80,10 +82,10 @@
   in
     if full
     then write_list ("Assertions of Boogie verification condition " ^
-      quote vc_name ^ ":") Pretty.str (sort fast_string_ord
+      quote vc_name ^ ":") Pretty.str (sort prefix_string_ord
         (map (pretty "proved") ps @ map (pretty "not proved") us))
     else write_list ("Unproved assertions of Boogie verification condition " ^
-      quote vc_name ^ ":") Pretty.str (sort fast_string_ord us)
+      quote vc_name ^ ":") Pretty.str (sort prefix_string_ord us)
   end
 
 
@@ -147,7 +149,7 @@
     then writeln ("Completely solved Boogie verification condition " ^
       quote vc_name ^ ".")
     else write_list ("Unsolved assertions of Boogie verification condition " ^
-      quote vc_name ^ ":") Pretty.str (sort fast_string_ord unsolved)
+      quote vc_name ^ ":") Pretty.str (sort prefix_string_ord unsolved)
   end
 end