src/HOL/Boogie/Tools/boogie_loader.ML
changeset 34959 cd7c98fdab80
parent 34181 003333ffa543
child 35125 acace7e30357
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jan 21 09:27:57 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jan 22 16:33:44 2010 +0100
     1.3 @@ -30,8 +30,14 @@
     1.4        | _   => ("_" ^ string_of_int (ord s) ^ "_"))
     1.5    in prefix "b_" o translate_string purge end
     1.6  
     1.7 +fun drop_underscore s =
     1.8 +  try (unsuffix "_") s
     1.9 +  |> Option.map drop_underscore
    1.10 +  |> the_default s
    1.11 +
    1.12  val short_name =
    1.13 -  translate_string (fn s => if Symbol.is_letdig s then s else "")
    1.14 +  translate_string (fn s => if Symbol.is_letdig s then s else "") #>
    1.15 +  drop_underscore
    1.16  
    1.17  (* these prefixes must be distinct: *)
    1.18  val var_prefix = "V_"