# HG changeset patch
# User boehmes
# Date 1264174424 -3600
# Node ID cd7c98fdab809bcb7ea3bfba1208d9d5974c8e10
# Parent  d62eddd9e253814e1d28ee0d0e32b1c02582f352
drop underscores at end of names coming from Boogie

diff -r d62eddd9e253 -r cd7c98fdab80 src/HOL/Boogie/Tools/boogie_loader.ML
--- 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_"