drop underscores at end of names coming from Boogie

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jan 21 09:27:57 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jan 22 16:33:44 2010 +0100
@@ -30,8 +30,14 @@
       | _   => ("_" ^ string_of_int (ord s) ^ "_"))
   in prefix "b_" o translate_string purge end
 
+fun drop_underscore s =
+  try (unsuffix "_") s
+  |> Option.map drop_underscore
+  |> the_default s
+
 val short_name =
-  translate_string (fn s => if Symbol.is_letdig s then s else "")
+  translate_string (fn s => if Symbol.is_letdig s then s else "") #>
+  drop_underscore
 
 (* these prefixes must be distinct: *)
 val var_prefix = "V_"