src/HOL/SPARK/Tools/spark_vcs.ML
changeset 47880 7e202f71a249
parent 46725 d34ec0512dfb
child 48167 da1a1eae93fa
     1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Feb 28 11:10:09 2012 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri May 11 13:41:30 2012 +0200
     1.3 @@ -1066,7 +1066,7 @@
     1.4          Symtab.update ("true", (@{term True}, booleanN)),
     1.5          Name.context),
     1.6         thy |> Sign.add_path
     1.7 -         (if prfx = "" then Long_Name.base_name ident else prfx)) |>
     1.8 +         ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
     1.9        fold (add_type_def prfx) (items types) |>
    1.10        fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
    1.11          ids_thy |>