# HG changeset patch
# User berghofe
# Date 1330335159 -3600
# Node ID 5759ecd5c9059112ad6dc1e5215563ae5aa36996
# Parent  28a01ea3523a2aaecb174d44bc3460fde391fae4
Use long prefix rather than short package name to disambiguate constant names
introduced by verification environment

diff -r 28a01ea3523a -r 5759ecd5c905 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Feb 26 21:44:12 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Feb 27 10:32:39 2012 +0100
@@ -1027,7 +1027,8 @@
         Symtab.update ("false", (@{term False}, booleanN)) |>
         Symtab.update ("true", (@{term True}, booleanN)),
         Name.context),
-       thy |> Sign.add_path (Long_Name.base_name ident)) |>
+       thy |> Sign.add_path
+         (if prfx = "" then Long_Name.base_name ident else prfx)) |>
       fold (add_type_def prfx) (items types) |>
       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
         ids_thy |>