# HG changeset patch
# User boehmes
# Date 1260743857 -3600
# Node ID 3edfefaaf355b62569a96d9d9bb49033770d3c83
# Parent  ada58d8137835ffb41a8b88c8ef484a52d43d0ec
print assertions in a more natural order

diff -r ada58d813783 -r 3edfefaaf355 src/HOL/Boogie/Tools/boogie_commands.ML
--- 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