# HG changeset patch
# User berghofe
# Date 1336736490 -7200
# Node ID 7e202f71a24915b224d496a969c9fc6ebeafa18c
# Parent  de5602637ab4f36535bc8b224b8d0da7d16427e4
Fixed disambiguation of names (cf. 5759ecd5c905)

diff -r de5602637ab4 -r 7e202f71a249 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu May 10 22:51:44 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri May 11 13:41:30 2012 +0200
@@ -1066,7 +1066,7 @@
         Symtab.update ("true", (@{term True}, booleanN)),
         Name.context),
        thy |> Sign.add_path
-         (if prfx = "" then Long_Name.base_name ident else prfx)) |>
+         ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
       fold (add_type_def prfx) (items types) |>
       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
         ids_thy |>