# 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 |>